Bug fixing + cosmetic changes

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

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 3948a730fb3906f9640cff860e5e0630171706ec..1b97b15cf893c9c42f513e34a533554d8336104b 100644 (file)
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -161,7 +161,7 @@ function trace_of(node) {
 
 function changeFile(name) {
     current_fname = name;
-    matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+    matitaTitle.innerHTML = "cic:/matita/" + name;
     baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
 }
 
@@ -302,7 +302,7 @@ function strip_interpr() {
 }
 
 function strip_anchors() {
-       strip_tags("INPUT","anchor");
+       strip_tags("IMG","anchor");
 }
  
 function keypress(e)
@@ -655,21 +655,23 @@ function advOneStep(xml) {
         if (is_defined(parsed)) {
        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
            var len = parseInt(parsed.getAttribute("length"));
-            // len0 = unlocked.innerHTML.length;
-           var unescaped = unlocked.innerHTML.html_to_matita();
-           var parsedtxt = parsed.childNodes[0].wholeText;
-           //parsedtxt = unescaped.substr(0,len); 
-           var unparsedtxt = unescaped.substr(len);
-           lockedbackup += parsedtxt;
-           locked.innerHTML = lockedbackup;
-           unlocked.innerHTML = unparsedtxt.matita_to_html();
-           // len1 = unlocked.innerHTML.length;
-           // len2 = len0 - len1;
-           var len2 = parsedtxt.length;
-           metasenv = xml.getElementsByTagName("meta");
-           statements = listcons(len2,statements);
-           //unlocked.scrollIntoView(true);
-           smartScroll();
+           if (len > 0) {
+              // len0 = unlocked.innerHTML.length;
+             var unescaped = unlocked.innerHTML.html_to_matita();
+             var parsedtxt = parsed.childNodes[0].wholeText;
+             //parsedtxt = unescaped.substr(0,len); 
+             var unparsedtxt = unescaped.substr(len);
+             lockedbackup += parsedtxt;
+             locked.innerHTML = lockedbackup;
+             unlocked.innerHTML = unparsedtxt.matita_to_html();
+             // len1 = unlocked.innerHTML.length;
+             // len2 = len0 - len1;
+             var len2 = parsedtxt.length;
+             metasenv = xml.getElementsByTagName("meta");
+             statements = listcons(len2,statements);
+             //unlocked.scrollIntoView(true);
+             smartScroll();
+           }
            return len;
        }
        else if (is_defined(ambiguity)) {
@@ -1118,7 +1120,7 @@ function gotoPos(offset)
                if (is_defined(xml)) {
                    try {
                        var len = advOneStep(xml);
-                       if (offset <= len) {
+                       if (len == 0 || offset <= len) {
                                init_hyperlinks();
                                init_autotraces();
                                populate_goalarray(metasenv);
@@ -1147,6 +1149,7 @@ function gotoPos(offset)
 
 function retractStep()
 {
+    if (!is_nil(statements)) {
        processor = function(xml) {
                if (typeof xml != "undefined") {
                        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
@@ -1177,6 +1180,7 @@ function retractStep()
        };
        pause();
         callServer("retract",processor);
+    }
 }
 
 function openFile()
@@ -1219,7 +1223,7 @@ function retrieveFile(thefile)
                        strip_anchors();
                        init_hyperlinks();
                        init_autotraces();
-
+                       unlocked.scrollIntoView(true);
                   } else {
                        error("file open failed");
                   }
@@ -1249,7 +1253,7 @@ function go_external_hyperlink(uri,thefile,id)
                         $('#locked').html(doctext);
                         try {
                          // scroll to anchor (if it exists)
-                         $('#' + id).scrollIntoView(true);
+                         $('#' + id).get(0).scrollIntoView(true);
                         } catch (e) { }
                         init_hyperlinks();
                         init_autotraces();
@@ -1446,12 +1450,12 @@ function createDir() {
 function commitAll()
 {
        processor = function(xml) {
-               if (is_defined(xml)) {
+               if (xml.getElementsByTagName("details").length > 0) {
                         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 {
-                       alert("Commit failed!");
+                       alert("Commit denied.\nPermission to commit and update is provided by the Matita team upon request.");
                }
                resume();
        };
@@ -1462,12 +1466,12 @@ function commitAll()
 function updateAll()
 {
        processor = function(xml) {
-               if (is_defined(xml)) {
+               if (xml.getElementsByTagName("details").length > 0) {
                        alert("Update executed.\n\n" +
                               "Details:\n" +
                               xml.getElementsByTagName("details")[0].textContent);
                } else {
-                       alert("Update failed!");
+                       alert("Update denied.\nPermission to commit and update is provided by the Matita team upon request.");
                }
                resume();
        };