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=248eeaa672b157072d771b7e4d89c9a32ee9488d;hb=31dccba27d8819bc5e4b9ad3fc6f244f4dfbfbc0;hp=1b97b15cf893c9c42f513e34a533554d8336104b;hpb=80b2ee96ffe418af9c39d3714e2a2f1dc74dab41;p=helm.git

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 1b97b15cf..248eeaa67 100644
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -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++) {
@@ -652,6 +652,7 @@ 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"));
@@ -743,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";
 	}
 
 }
@@ -1381,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);
 }
@@ -1437,6 +1442,7 @@ function createDir() {
 		} else {
                       alert("An error occurred :-(");
 		}
+                resume();
                 dialogBox.reload();
 	};
         pause();