From eb553660052f5853a7baeb6905dccd59abc0f8e4 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 13 Dec 2011 11:40:23 +0000
Subject: [PATCH] Matitaweb: clicking buttons disables the GUI to prevent
 another operation from being issued before the first one has completed.

---
 matitaB/matita/matitaweb.js | 55 +++++++++++++++++++++++++------------
 1 file changed, 37 insertions(+), 18 deletions(-)

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 6e6b905db..23bf4d396 100644
--- 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();
+}
+
-- 
2.39.2