X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;fp=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=1b97b15cf893c9c42f513e34a533554d8336104b;hb=92fc70ae76ae4376b7976d1dff5c9b57d1b96056;hp=3948a730fb3906f9640cff860e5e0630171706ec;hpb=c0ac63fead67ea1902e3d923ce877a2779cf501e;p=helm.git

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 3948a730f..1b97b15cf 100644
--- 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();
 	};