Matitaweb: clicking buttons disables the GUI to prevent another operation from

being issued before the first one has completed.

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 6e6b905dba52173bdac9fc007b5ec872a413f4c5..23bf4d396c62acba6d861c1d96485fa381e7109f 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -497,22 +497,6 @@ String.prototype.matita_to_html = function()
        return (unescape(result));
 }
 
-function pause()
-{
-       advanceButton.disabled = true;
-        retractButton.disabled = true;
-        cursorButton.disabled = true;
-        bottomButton.disabled = true;
-}
-
-function resume()
-{
-       advanceButton.disabled = false;
-        retractButton.disabled = false;
-        cursorButton.disabled = false;
-        bottomButton.disabled = false;
-}
-
 function is_defined(x)
 {
        return (typeof x != "undefined");
@@ -1424,7 +1408,8 @@ function get_checked_index(name) {
 
 function cancel_disambiguate() {
        matita.disambMode = false;
-       $('#whitemask').hide();
+       enable_toparea();
+       enable_editing();
        updateSide();
 }
 
@@ -1451,7 +1436,8 @@ function do_disambiguate() {
            unlocked.innerHTML = pre + mid + post;
 
            matita.disambMode = false;
-           $('#whitemask').hide();
+           enable_toparea();
+           enable_editing();
            updateSide();
        }
 }
@@ -1512,3 +1498,36 @@ function disable_toparea() {
         $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
        $('#whitemask').fadeTo('fast',0.7);
 }
+
+function enable_toparea() {
+       $('#whitemask').hide();
+}
+
+function disable_editing() {
+       unlocked.contentEditable = false;
+}
+
+function enable_editing() {
+       unlocked.contentEditable = true;
+}
+
+function pause()
+{
+       // advanceButton.disabled = true;
+        // retractButton.disabled = true;
+        // cursorButton.disabled = true;
+        // bottomButton.disabled = true;
+       disable_toparea();
+       disable_editing();
+}
+
+function resume()
+{
+       // advanceButton.disabled = false;
+        // retractButton.disabled = false;
+        // cursorButton.disabled = false;
+        // bottomButton.disabled = false;
+       enable_toparea();
+       enable_editing();
+}
+