Matitaweb: added preliminary support for interactive disambiguation.

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 349097719c405584c88f49a166e99c6ebac399e2..ccb2f37445fabf8e38332df2fc714e9d5fffbf6e 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -33,11 +33,22 @@ function unescape_html(s)
   return text_of_html(u)
 }
 
+function filterByClass (elements,class){
+  var itemsfound = new Array;
+  for(var i=0;i<elements.length;i++){
+    if(elements[i].className == class){
+      itemsfound.push(elements[i]);
+    }
+  }
+  return itemsfound;
+}
+
 function initialize()
 {
   if (readCookie("session") == null) {
     window.location = "/login.html"
   } else {
+    matitaTitle = document.getElementById("matitaTitle");
     locked = document.getElementById("locked");
     unlocked = document.getElementById("unlocked");
     workarea = document.getElementById("workarea");
@@ -54,6 +65,8 @@ function initialize()
     dialogBox = document.getElementById("dialogBox");
     dialogTitle = document.getElementById("dialogTitle");
     dialogContent = document.getElementById("dialogContent");
+
+    changeFile("test.ma");
   
     // hide sequent view at start
     hideSequent();
@@ -63,6 +76,11 @@ function initialize()
   }
 }
 
+function changeFile(name) {
+    current_fname = name;
+    matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+}
+
 function init_keyboard(target)
 {
     if (target.addEventListener)
@@ -153,12 +171,25 @@ function lookup_tex(texmacro)
   texmacro = texmacro.substring(1);
   return unescape(macro2utf8[texmacro]);
 }
+
+function strip_errors() 
+{
+    errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
+    for (i = 0; i < errors.length; i++) {
+        children = errors[i].childNodes;
+        for (j = 0; j < children.length; j++) {
+            unlocked.insertBefore(children[j],errors[i]);
+       }
+        unlocked.removeChild(errors[i]);
+    }
+}
  
 function keypress(e)
 {
    if (!e) e= event;
    pressmesg('keypress',e);
    var s = string_of_key(e.charCode);
+   strip_errors();
    if (s == " ") {
        j = getCursorPos();
        i = unlocked.innerHTML.lastIndexOf('\\',j);
@@ -202,7 +233,7 @@ function debug(txt)
        // but google chrome's innerText is, in a sense, "write only"
        // what should we do?
         // logarea.innerText = txt + "\n" + logarea.innerText;
-        logtxt = logtxt + "\n" + txt;
+        logtxt = /* logtxt + "\n" +*/ txt;
 }
 
 function showLog() {
@@ -392,12 +423,14 @@ String.prototype.html_to_matita = function()
        var patt3 = />/gi
        var patt4 = /&lt;/gi;
        var patt5 = /&gt;/gi;
+       var patt6 = /&nbsp;/gi;
        var result = this;
        result = result.replace(patt1,"\n");
        result = result.replace(patt2,"\005");
        result = result.replace(patt3,"\006");
        result = result.replace(patt4,"<");
        result = result.replace(patt5,">");
+       result = result.replace(patt6," ");
        return (unescape(result));
 }
 
@@ -502,24 +535,31 @@ function advanceForm1()
 {
        processor = function(xml) {
                if (is_defined(xml)) {
+                        parsed = xml.getElementsByTagName("parsed")[0];
+                        if (is_defined(parsed)) {
                        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-                       parsed = xml.getElementsByTagName("parsed")[0];
-                       len = parseInt(parsed.getAttribute("length"));
-                       // len0 = unlocked.innerHTML.length;
-                       unescaped = unlocked.innerHTML.html_to_matita();
-                       parsedtxt = parsed.childNodes[0].nodeValue;
-                       //parsedtxt = unescaped.substr(0,len); 
-                       unparsedtxt = unescaped.substr(len);
-                       lockedbackup += parsedtxt;
-                       locked.innerHTML = lockedbackup;
-                       unlocked.innerHTML = unparsedtxt.matita_to_html();
-                       // len1 = unlocked.innerHTML.length;
-                       // len2 = len0 - len1;
-                       len2 = parsedtxt.length;
-                       metasenv = xml.getElementsByTagName("meta");
-                       populate_goalarray(metasenv);
-                       statements = listcons(len2,statements);
-                       unlocked.scrollIntoView(true);
+                           len = parseInt(parsed.getAttribute("length"));
+                           // len0 = unlocked.innerHTML.length;
+                           unescaped = unlocked.innerHTML.html_to_matita();
+                           parsedtxt = parsed.childNodes[0].nodeValue;
+                           //parsedtxt = unescaped.substr(0,len); 
+                           unparsedtxt = unescaped.substr(len);
+                           lockedbackup += parsedtxt;
+                           locked.innerHTML = lockedbackup;
+                           unlocked.innerHTML = unparsedtxt.matita_to_html();
+                           // len1 = unlocked.innerHTML.length;
+                           // len2 = len0 - len1;
+                           len2 = parsedtxt.length;
+                           metasenv = xml.getElementsByTagName("meta");
+                           populate_goalarray(metasenv);
+                           statements = listcons(len2,statements);
+                           unlocked.scrollIntoView(true);
+                       }
+                       else {
+                            error = xml.getElementsByTagName("error")[0]; 
+                           unlocked.innerHTML = error.childNodes[0].nodeValue;
+                           // debug(xml.childNodes[0].nodeValue);
+                       }
                } else {
                        debug("advance failed");
                }
@@ -688,14 +728,18 @@ function retrieveFile(thefile)
        processor = function(xml)
        {
                if (is_defined(xml)) {  
-                       current_fname = thefile;
+                       changeFile(thefile);
                        lockedbackup = ""
                        locked.innerHTML = lockedbackup;
                         // code originally used in google chrome (problems with mozilla)
                        // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
                        // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
                        debug(xml.childNodes[0].textContent);
-                       unlocked.innerHTML = xml.childNodes[0].textContent;
+                        if (document.all) { // IE
+                          unlocked.innerHTML = xml.childNodes[0].text;
+                        } else {
+                          unlocked.innerHTML = xml.childNodes[0].textContent;
+                        }
 
                } else {
                        debug("file open failed");
@@ -816,7 +860,6 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
            // when force is true, reloadDialog is not needed 
         }
        processor = function(xml) {
-               current_fname = fname;
                if (is_defined(xml)) {
                  if (xml.childNodes[0].textContent != "ok") {
                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
@@ -825,7 +868,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
                       reloadDialog();
                    }
                  } else {
-                   current_fname = fname;
+                   changeFile(fname);
                    debug("file saved!");
                     if (reloadFile) { retrieveFile(fname); }
                  }
@@ -870,9 +913,11 @@ function commitAll()
 {
        processor = function(xml) {
                if (is_defined(xml)) {
-                       debug("commit succeeded(?)");
+                        debug(xml.getElementsByTagName("details")[0].textContent);
+                       alert("Commit executed: see details in the log.\n\n" +
+                              "NOTICE: this message does NOT imply (yet) that the commit was successful.");
                } else {
-                       debug("commit failed!");
+                       alert("Commit failed!");
                }
                resume();
        };
@@ -884,9 +929,11 @@ function updateAll()
 {
        processor = function(xml) {
                if (is_defined(xml)) {
-                       debug("update succeeded(?)");
+                       alert("Update executed.\n\n" +
+                              "Details:\n" +
+                              xml.getElementsByTagName("details")[0].textContent);
                } else {
-                       debug("update failed!");
+                       alert("Update failed!");
                }
                resume();
        };