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

[helm.git] / matitaB / matita / matitaweb.js

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 343d539e66deda5c23cc8a963430f0f693bb72c5..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");
@@ -708,8 +692,10 @@ function get_choice_opts(i) {
       var desc;
       if (is_defined(title)) {
           desc = title;
-      } else {
+      } else if (is_defined(href)) {
           desc = href;
+      } else {
+          desc = "Preliminary error";
       }
   
       res[j] = document.createElement("input");
@@ -815,7 +801,7 @@ function show_failures() {
        var choicedesc = choice.getAttribute("desc");
 
        var title = "<H3>Disambiguation failed</H3>";
-       var subtitle = "<p>Errors at node " + choiceno + " = " + choicedesc + "</p>";
+       var subtitle = "<p>Errors at node " + cpno + " = " + choicedesc + "</p>";
 
        disambcell.innerHTML = title + subtitle;
        var failures = get_failure_opts(cpno,choiceno);
@@ -1422,7 +1408,8 @@ function get_checked_index(name) {
 
 function cancel_disambiguate() {
        matita.disambMode = false;
-       $('#whitemask').hide();
+       enable_toparea();
+       enable_editing();
        updateSide();
 }
 
@@ -1449,7 +1436,8 @@ function do_disambiguate() {
            unlocked.innerHTML = pre + mid + post;
 
            matita.disambMode = false;
-           $('#whitemask').hide();
+           enable_toparea();
+           enable_editing();
            updateSide();
        }
 }
@@ -1510,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();
+}
+