X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=248eeaa672b157072d771b7e4d89c9a32ee9488d;hb=7666f9dddfcaca5671dd25d3cd2095481968c7bf;hp=3948a730fb3906f9640cff860e5e0630171706ec;hpb=98827f140349f91cbd546491b233d6d5d3f335c3;p=helm.git

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 3948a730f..248eeaa67 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('.'));
 }
 
@@ -262,9 +262,9 @@ function strip_tags(tagname,classname)
 {
     var tags;
     if (is_defined(classname)) {
-      tags = $(tagname + "." + classname);
+      tags = $("#unlocked " + tagname + "." + classname);
     } else {
-      tags = $(tagname);
+      tags = $("#unlocked " + tagname);
     }
     var tlen = tags.length; // preserving the value from removeChild operations
     for (i = 0; i < tlen; i++) {
@@ -302,7 +302,7 @@ function strip_interpr() {
 }
 
 function strip_anchors() {
-	strip_tags("INPUT","anchor");
+	strip_tags("IMG","anchor");
 }
  
 function keypress(e)
@@ -652,24 +652,27 @@ function advOneStep(xml) {
         var parsed = xml.getElementsByTagName("parsed")[0];
 	var ambiguity = xml.getElementsByTagName("ambiguity")[0];
 	var disamberr = xml.getElementsByTagName("disamberror")[0];
+	var localized = xml.getElementsByTagName("localized")[0];
         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)) {
@@ -741,12 +744,14 @@ function advOneStep(xml) {
               next_cp(0);
             }
 	    throw "Stop";
-	}
-        else {
-            var error = xml.getElementsByTagName("error")[0]; 
-	    unlocked.innerHTML = error.childNodes[0].wholeText;
-	    error(xml.childNodes[0].nodeValue);
+	} else if (is_defined(localized)) {
+	    unlocked.innerHTML = localized.childNodes[0].wholeText;
 	    throw "Stop";
+        }
+        else {
+            var err = xml.getElementsByTagName("error")[0]; 
+            error(err.childNodes[0].nodeValue);
+            throw "Stop";
 	}
 
 }
@@ -1118,7 +1123,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 +1152,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 +1183,7 @@ function retractStep()
 	};
 	pause();
         callServer("retract",processor);
+    }
 }
 
 function openFile()
@@ -1219,7 +1226,7 @@ function retrieveFile(thefile)
 			strip_anchors();
 		        init_hyperlinks();
 			init_autotraces();
-
+			unlocked.scrollIntoView(true);
 		   } else {
 			error("file open failed");
 	           }
@@ -1249,7 +1256,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();
@@ -1377,7 +1384,9 @@ function newDialog()
 {
 	callback = function (fname) { 
 	  abortDialog("dialogBox");
-	  saveFile(fname,"","",false,newDialog,true);
+	  saveFile(fname,"",
+		   "(* new script *)",
+                   false,newDialog,true);
 	};
 	showLibrary("Create new file", callback, newDialog);
 }
@@ -1433,6 +1442,7 @@ function createDir() {
 		} else {
                       alert("An error occurred :-(");
 		}
+                resume();
                 dialogBox.reload();
 	};
         pause();
@@ -1446,12 +1456,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 +1472,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();
 	};