First attempt at svn commit of developments.

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index fb6c0869da5b9c6afac25648187987195215b07c..07dbb06f68c7ce6717b442fbc1c716551caff28f 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -15,6 +15,7 @@ var dialogBox;
 var dialogTitle;
 var dialogContent;
 var metasenv = "";
+var lockedbackup = "";
 
 function initialize()
 {
@@ -336,6 +337,8 @@ function switch_goal(meta)
   }
 }
 
+// the following is used to avoid escaping unicode, which results in 
+// the server being unable to unescape the string
 String.prototype.sescape = function() {
        var patt1 = /%/gi;
        var patt2 = /=/gi;
@@ -469,15 +472,17 @@ function advanceForm1()
                        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
                        parsed = xml.getElementsByTagName("parsed")[0];
                        len = parseInt(parsed.getAttribute("length"));
-                       len0 = unlocked.innerHTML.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);
-                       locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+                       lockedbackup += parsedtxt;
+                       locked.innerHTML = lockedbackup;
                        unlocked.innerHTML = unparsedtxt.matita_to_html();
-                       len1 = unlocked.innerHTML.length;
-                       len2 = len0 - len1;
+                       // len1 = unlocked.innerHTML.length;
+                       // len2 = len0 - len1;
+                       len2 = parsedtxt.length;
                        metasenv = xml.getElementsByTagName("meta");
                        populate_goalarray(metasenv);
                        statements = listcons(len2,statements);
@@ -499,19 +504,23 @@ function gotoBottom()
                        // debug("goto bottom: 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);
-                       locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
-                       unlocked.innerHTML = unparsedtxt.matita_to_html();
-                       len1 = unlocked.innerHTML.length;
-                       len2 = len0 - len1;
-                       metasenv = xml.getElementsByTagName("meta");
-                       populate_goalarray(metasenv);
-                       statements = listcons(len2,statements);
-                       unlocked.scrollIntoView(true);
+                       if (len > 0) {
+                         // 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; //.matita_to_html();
+                         unlocked.innerHTML = unparsedtxt.matita_to_html();
+                         // len1 = unlocked.innerHTML.length;
+                         len2 = parsedtxt.length;
+                         metasenv = xml.getElementsByTagName("meta");
+                         populate_goalarray(metasenv);
+                         if (len2 > 0)
+                           statements = listcons(len2,statements);
+                         unlocked.scrollIntoView(true);
+                       }
                } else {
                        debug("goto bottom failed");
                } 
@@ -532,15 +541,16 @@ function gotoPos(offset)
                if (is_defined(xml)) {
                        parsed = xml.getElementsByTagName("parsed")[0];
                        len = parseInt(parsed.getAttribute("length"));
-                       len0 = unlocked.innerHTML.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);
-                       locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+                       lockedbackup += parsedtxt;
+                       locked.innerHTML = lockedbackup; //.matita_to_html();
                        unlocked.innerHTML = unparsedtxt.matita_to_html();
-                       len1 = unlocked.innerHTML.length;
-                       len2 = len0 - len1;
+                       // len1 = unlocked.innerHTML.length;
+                       len2 = parsedtxt.length;
                        metasenv = xml.getElementsByTagName("meta");
                        // populate_goalarray(metasenv);
                        statements = listcons(len2,statements);
@@ -569,10 +579,17 @@ function retract()
                        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
                        statementlen = parseInt(listhd(statements));
                         statements = listtl(statements);
+                       /*
                         lockedlen = locked.innerHTML.length - statementlen;
                        statement = locked.innerHTML.substr(lockedlen, statementlen);
                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
                        unlocked.innerHTML = statement + unlocked.innerHTML;
+                       */
+                        lockedlen = lockedbackup.length - statementlen;
+                       statement = lockedbackup.substr(lockedlen, statementlen);
+                       lockedbackup = lockedbackup.substr(0,lockedlen);
+                        locked.innerHTML = lockedbackup;
+                       unlocked.innerHTML = statement + unlocked.innerHTML;
                        metasenv = xml.getElementsByTagName("meta");
                         populate_goalarray(metasenv);
                         unlocked.scrollIntoView(true);
@@ -592,7 +609,8 @@ function openFile()
        processor = function(xml)
        {
                if (is_defined(xml)) {  
-                       locked.innerHTML = "";
+                       lockedbackup = "";
+                       locked.innerHTML = lockedbackup;
                        unlocked.innerHTML = xml.documentElement.textContent;
                } else {
                        debug("file open failed");
@@ -606,7 +624,8 @@ function retrieveFile(thefile)
        processor = function(xml)
        {
                if (is_defined(xml)) {  
-                       locked.innerHTML = "";
+                       lockedbackup = ""
+                       locked.innerHTML = lockedbackup;
                        debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
                        unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
 
@@ -615,6 +634,7 @@ function retrieveFile(thefile)
                }
        };
        dialogBox.style.display = "none";
+       current_fname = thefile;
        callServer("open",processor,"file=" + escape(thefile)); 
 }
 
@@ -659,6 +679,39 @@ function showLibrary()
   
 }
 
+function saveFile()
+{
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                       debug("file saved!");
+               } else {
+                       debug("save file failed");
+               }
+               resume();
+       };
+       if (is_defined(current_fname)) {
+          pause();
+          callServer("save",processor,"file=" + escape(current_fname) + 
+                                   "&locked=" + (locked.innerHTML.html_to_matita()).sescape() +
+                                   "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape());
+       }
+       else { debug("no file selected"); }
+}
+
+function commitAll()
+{
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                       debug("commit succeeded(?)");
+               } else {
+                       debug("commit failed!");
+               }
+               resume();
+       };
+        pause();
+        callServer("commit",processor);
+}
+
 var goalcell;
 
 function hideSequent() {