Matitaweb: goto bottom can now be undone step by step and also reports errors

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index cd1e624e1fba6664db95a222bdfd426a593e00ae..d1480e72d744088a41881c32c6f4b33f9caaf502 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -317,6 +317,9 @@ function listnil()
        return ("");
 }
 
+function list_append(l1,l2)
+{ return (l1 + l2) }
+
 function is_nil(l)
 {
        return (l == "");
@@ -588,7 +591,7 @@ function advanceForm1()
                            var len = parseInt(parsed.getAttribute("length"));
                            // len0 = unlocked.innerHTML.length;
                            var unescaped = unlocked.innerHTML.html_to_matita();
-                           var parsedtxt = parsed.childNodes[0].nodeValue;
+                           var parsedtxt = parsed.childNodes[0].wholeText;
                            //parsedtxt = unescaped.substr(0,len); 
                            var unparsedtxt = unescaped.substr(len);
                            lockedbackup += parsedtxt;
@@ -665,7 +668,7 @@ function advanceForm1()
                        }
                        else {
                             var error = xml.getElementsByTagName("error")[0]; 
-                           unlocked.innerHTML = error.childNodes[0].nodeValue;
+                           unlocked.innerHTML = error.childNodes[0].wholeText;
                            // debug(xml.childNodes[0].nodeValue);
                        }
                } else {
@@ -683,27 +686,95 @@ function gotoBottom()
        processor = function(xml) {
                if (is_defined(xml)) {
                        // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
-                       parsed = xml.getElementsByTagName("parsed")[0];
-                       len = parseInt(parsed.getAttribute("length"));
-                       if (len > 0) {
+                       var parsed = xml.getElementsByTagName("parsed");
+                       var localized = xml.getElementsByTagName("localized")[0];
+                       var ambiguity = xml.getElementsByTagName("ambiguity")[0];
+                       var generic_err = xml.getElementsByTagName("error")[0];
+                       for (var i = 0;i < parsed.length; i++) {
+                         var len = parsed[i].getAttribute("length");
                          // len0 = unlocked.innerHTML.length;
-                         unescaped = unlocked.innerHTML.html_to_matita();
-                          // not working in mozilla
-                         // parsedtxt = parsed.childNodes[0].nodeValue;
-                         parsedtxt = parsed.childNodes[0].wholeText;
+                         var unescaped = unlocked.innerHTML.html_to_matita();
+                         // the browser may decide to split textnodes: use wholeText!
+                         var parsedtxt = parsed[i].childNodes[0].wholeText;
                          //parsedtxt = unescaped.substr(0,len); 
-                         unparsedtxt = unescaped.substr(len);
+                         var unparsedtxt = unescaped.substr(len);
                          lockedbackup += parsedtxt;
                          locked.innerHTML = lockedbackup; //.matita_to_html();
                          unlocked.innerHTML = unparsedtxt.matita_to_html();
                          // len1 = unlocked.innerHTML.length;
-                         len2 = parsedtxt.length;
-                         metasenv = xml.getElementsByTagName("meta");
-                         init_autotraces();
-                         populate_goalarray(metasenv);
-                         if (len2 > 0)
-                           statements = listcons(len2,statements);
-                         unlocked.scrollIntoView(true);
+                         var len2 = parsedtxt.length;
+                         statements = listcons(len2,statements);
+                       }
+                       unlocked.scrollIntoView(true);
+                       metasenv = xml.getElementsByTagName("meta");
+                       init_autotraces();
+                       populate_goalarray(metasenv);
+
+                       if (is_defined(ambiguity)) {
+                           var start = parseInt(ambiguity.getAttribute("start"));
+                           var stop = parseInt(ambiguity.getAttribute("stop"));
+                           var choices = xml.getElementsByTagName("choice");
+
+                           matita.ambiguityStart = start;
+                           matita.ambiguityStop = stop;
+                           matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
+                           matita.interpretations = [];
+                       
+                           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;
+
+                           var title = "<H3>Ambiguous input</H3>";
+                           disambcell.innerHTML = title;
+                           for (i = 0;i < choices.length;i++) {
+                               matita.interpretations[i] = new Object();
+
+                               var href = choices[i].getAttribute("href");
+                               var title = choices[i].getAttribute("title");
+                               var desc = choices[i].childNodes[0].nodeValue;
+
+                               matita.interpretations[i].href = href;
+                               matita.interpretations[i].title = title;
+                               matita.interpretations[i].desc = desc;
+                               
+                               var choice = document.createElement("input");
+                               choice.setAttribute("type","radio");
+                               choice.setAttribute("name","interpr");
+                               choice.setAttribute("href",href);
+                               choice.setAttribute("title",title);
+                               if (i == 0) choice.setAttribute("checked","");
+                               
+                               disambcell.appendChild(choice);
+                               disambcell.appendChild(document.createTextNode(desc));
+                               disambcell.appendChild(document.createElement("br"));
+                           }
+
+                           var okbutton = document.createElement("input");
+                           okbutton.setAttribute("type","button");
+                           okbutton.setAttribute("value","OK");
+                           okbutton.setAttribute("onclick","do_disambiguate()");
+                           var cancelbutton = document.createElement("input");
+                           cancelbutton.setAttribute("type","button");
+                           cancelbutton.setAttribute("value","Cancel");
+                           cancelbutton.setAttribute("onclick","cancel_disambiguate()");
+
+                           disambcell.appendChild(okbutton);
+                           disambcell.appendChild(cancelbutton);
+
+                           disable_toparea();
+
+                           matita.disambMode = true;
+                           updateSide();
+                       }
+                       if (is_defined(localized)) {
+                           unlocked.innerHTML = localized.wholeText;
+                       }
+                       if (is_defined(generic_err)) {
+                           debug("Unmanaged error:\n" ^ generic_err.wholeText);
                        }
                } else {
                        debug("goto bottom failed");
@@ -712,7 +783,6 @@ function gotoBottom()
        };
        pause();
        callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
-  
 }
 
 
@@ -757,7 +827,7 @@ function gotoPos(offset)
                        len = parseInt(parsed.getAttribute("length"));
                        // len0 = unlocked.innerHTML.length;
                        unescaped = unlocked.innerHTML.html_to_matita();
-                       parsedtxt = parsed.childNodes[0].nodeValue;
+                       parsedtxt = parsed.childNodes[0].wholeText;
                        //parsedtxt = unescaped.substr(0,len); 
                        unparsedtxt = unescaped.substr(len);
                        lockedbackup += parsedtxt;