X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=44fd608a1bbf7b099f495a2789cb6a0242fb1af9;hb=6c84daf943dfba98f3061cba6adadc8837bf150a;hp=890b34ec0b8cef0982f5b703e35ce8470130b30d;hpb=31a709773b66950ce7f14fed8fa4a951a4673ee9;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 890b34ec0..44fd608a1 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -575,13 +575,13 @@ function advanceForm1()
 
 			    matita.ambiguityStart = start;
 			    matita.ambiguityStop = stop;
-			    matita.unlockedbackup = unlocked.innerHTML;
+			    matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 			    matita.interpretations = [];
 			
-			    var unlockedtxt = unlocked.innerHTML;
-			    var pre = unlockedtxt.substring(0,start);
-			    var mid = unlockedtxt.substring(start,stop);
-			    var post = unlockedtxt.substring(stop);
+			    var unlockedtxt = unlocked.innerHTML.html_to_matita();
+			    var pre = unlockedtxt.substring(0,start).matita_to_html();
+			    var mid = unlockedtxt.substring(start,stop).matita_to_html();
+			    var post = unlockedtxt.substring(stop).matita_to_html();
 			    unlocked.innerHTML = pre + 
 				    "<span class=\"error\" title=\"disambiguation error\">" +
 				    mid + "</span>" + post;
@@ -618,7 +618,7 @@ function advanceForm1()
 			    var cancelbutton = document.createElement("input");
 			    cancelbutton.setAttribute("type","button");
 			    cancelbutton.setAttribute("value","Cancel");
-			    cancelbutton.setAttribute("onclick","void(0)");
+			    cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 
 			    disambcell.appendChild(okbutton);
 			    disambcell.appendChild(cancelbutton);
@@ -1106,12 +1106,21 @@ function get_checked_index(name) {
 	return null;
 }
 
+function cancel_disambiguate() {
+	matita.disambMode = false;
+	updateSide();
+}
+
 function do_disambiguate() {
 	var i = get_checked_index("interpr");
 	if (i != null) {
-	    var pre = matita.unlockedbackup.substring(0,matita.ambiguityStart);
-	    var mid = matita.unlockedbackup.substring(matita.ambiguityStart,matita.ambiguityStop);
-	    var post = matita.unlockedbackup.substring(matita.ambiguityStop);
+	    var pre = matita.unlockedbackup
+		      .substring(0,matita.ambiguityStart).matita_to_html();
+	    var mid = matita.unlockedbackup
+		      .substring(matita.ambiguityStart,matita.ambiguityStop)
+		      .matita_to_html();
+	    var post = matita.unlockedbackup
+		       .substring(matita.ambiguityStop).matita_to_html();
 
 	    var href = matita.interpretations[i].href;
 	    var title = matita.interpretations[i].title;