From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 27 Oct 2011 11:32:11 +0000 (+0000)
Subject: Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
X-Git-Tag: make_still_working~2155
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6c84daf943dfba98f3061cba6adadc8837bf150a

Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Added pretty-printing of unhandled NTacStatus.Error exceptions.
---

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 9fc2b1bbc..a53d24f67 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -363,6 +363,14 @@ let advance0 sid text =
       let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita marked) in
       raise (Emphasized_error marked) 
+    | NTacStatus.Error (s,None) as e ->
+        prerr_endline 
+          ("NTacStatus.Error " ^ (Lazy.force s));
+        raise e
+    | NTacStatus.Error (s,Some exc) as e ->
+        prerr_endline 
+          ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
+        raise e
     | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
       let x,y = HExtlib.loc_of_floc loc in
       let choice_of_alias = function
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;