]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitaweb.js
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Matitaweb: Save as...
[helm.git] / matitaB / matita / matitaweb.js
diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index fb6c0869da5b9c6afac25648187987195215b07c..48acfe13e223a0118b03b5d96ddc7b1a36250513 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()
 {
@@ -177,7 +178,8 @@ function debug(txt)
         // internet explorer (v.9) doesn't work with innerHTML
        // but google chrome's innerText is, in a sense, "write only"
        // what should we do?
-        logarea.innerText = txt + "\n" + logarea.innerText;
+        // logarea.innerText = txt + "\n" + logarea.innerText;
+        logarea.innerHTML = txt; // + "\n" + logarea.innerText;
 }
 
 function listhd(l)
@@ -336,6 +338,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 +473,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 +505,25 @@ 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();
+                          // not working in mozilla
+                         // parsedtxt = parsed.childNodes[0].nodeValue;
+                         parsedtxt = parsed.childNodes[0].wholeText;
+                         //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 +544,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 +582,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,8 +612,9 @@ function openFile()
        processor = function(xml)
        {
                if (is_defined(xml)) {  
-                       locked.innerHTML = "";
-                       unlocked.innerHTML = xml.documentElement.textContent;
+                       lockedbackup = "";
+                       locked.innerHTML = lockedbackup;
+                       unlocked.innerHTML = xml.documentElement.wholeText;
                } else {
                        debug("file open failed");
                }
@@ -606,19 +627,24 @@ function retrieveFile(thefile)
        processor = function(xml)
        {
                if (is_defined(xml)) {  
-                       locked.innerHTML = "";
-                       debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
-                       unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
+                       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;
 
                } else {
                        debug("file open failed");
                }
        };
        dialogBox.style.display = "none";
+       current_fname = thefile;
        callServer("open",processor,"file=" + escape(thefile)); 
 }
 
-function showLibrary()
+function showLibrary(title,callback)
 { 
        var req = null; 
         // pause();
@@ -649,7 +675,7 @@ function showLibrary()
                        if(stat == 200)
                        {
                          debug(req.responseText);
-                         showDialog("<H2>Library</H2>",req.responseText);
+                         showDialog("<H2>" + title + "</H2>",req.responseText, callback);
                        } 
                } 
        };
@@ -659,6 +685,66 @@ function showLibrary()
   
 }
 
+function openDialog()
+{  
+       callback = function (fname) { retrieveFile(fname); };
+       showLibrary("Open file", callback);
+}
+
+function saveDialog()
+{  
+       callback = function (fname) { 
+         dialogBox.style.display = "none";
+         current_fname = fname;
+          saveFile(fname,false); 
+        };
+       showLibrary("Save file as", callback);
+}
+
+function saveFile(fname,force)
+{
+        if (!is_defined(fname)) {
+            fname = current_fname;
+        }
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                 if (xml.childNodes[0].textContent != "ok") {
+                    if (confirm("File already exists. Do you want to proceed anyway?")) {
+                       saveFile(fname,true);
+                   } else {
+                      saveDialog();
+                   }
+                 } else
+                       debug("file saved!");
+               } else {
+                       debug("save file failed");
+               }
+               resume();
+       };
+       if (is_defined(fname)) {
+          pause();
+          callServer("save",processor,"file=" + escape(fname) + 
+                                   "&locked=" + (locked.innerHTML.html_to_matita()).sescape() +
+                                   "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape() +
+                                   "&force=" + force);
+       }
+       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() {
@@ -671,10 +757,11 @@ function showSequent() {
   workarea.appendChild(goalcell);
 }
 
-function showDialog(title,content) {
+function showDialog(title,content,callback) {
   dialogTitle.innerHTML = title;
   dialogContent.innerHTML = content;
   dialogBox.style.display = "block";
+  dialogBox.callback = callback;
 }
 
 function removeElement(id) {
Unnamed repository; edit this file 'description' to name the repository.