Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.

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

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;