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 9fc2b1bbcf05b30e9cc327f39ba847dc0d29b5d4..a53d24f676ae3c3ec9a86e8182700e1a4aa9942c 100644 (file)
--- 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 890b34ec0b8cef0982f5b703e35ce8470130b30d..44fd608a1bbf7b099f495a2789cb6a0242fb1af9 100644 (file)
--- 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;