diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index 2e393fe..dfb38d7 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -5,6 +5,11 @@ function output_error(output_area, message) {
div.appendTo(output_area)
}
+// Reset the buttons on the editors to the "enabled" state
+function reset_buttons(editors){
+ editors.buttons.forEach(function(b){b.disabled = false;})
+}
+
// Process the result of a check
// editors: the editors to decorate
// output_area: the div where the messages should go
@@ -70,6 +75,8 @@ function process_check_output(editors, output_area, output, status, completed, m
// Congratulations!
if (completed) {
+ reset_buttons(editors);
+
if (status != 0) {
output_error(output_area, "exit status: " + status)
} else if (output_area.error_count == 0) {
@@ -121,6 +128,7 @@ function get_output_from_identifier(container, editors, output_area, identifier,
console.dir(xhr);
})
.fail(function (json) {
+ reset_buttons(editors);
output_error(output_area, json.message)
})
}
@@ -167,6 +175,7 @@ function query_operation_result(container, example_name, editors, output_area, o
})
.done(function (json) {
if (json.identifier == "") {
+ reset_buttons(editors)
output_error(output_area, json.message)
} else {
get_output_from_identifier(container, editors, output_area, json.identifier, 0)
@@ -337,10 +346,15 @@ function fill_editor_from_contents(container, example_name, example_server,
var output_area = $('
')
output_area.appendTo(output_div)
+ editors.buttons = []
+
if (container.attr("prove_button") || container.attr("run_button")){
var reset_button = $('