bug fixes

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

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 1b97b15cf893c9c42f513e34a533554d8336104b..248eeaa672b157072d771b7e4d89c9a32ee9488d 100644 (file)
--- 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();