X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=fedaaf7fbde482deb54024c25aa65e5834a816bf;hb=a7b54fb6f31e5ac626853890686ee54033dc7b24;hp=f0563928234812f20f980c467fc9b671784a1e6a;hpb=5a88ca4db8f9d97a58add90a8a23f06960d9364f;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index f05639282..fedaaf7fb 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -33,6 +33,16 @@ function unescape_html(s)
   return text_of_html(u)
 }
 
+function filterByClass (elements,class){
+  var itemsfound = new Array;
+  for(var i=0;i<elements.length;i++){
+    if(elements[i].className == class){
+      itemsfound.push(elements[i]);
+    }
+  }
+  return itemsfound;
+}
+
 function initialize()
 {
   if (readCookie("session") == null) {
@@ -161,12 +171,25 @@ function lookup_tex(texmacro)
   texmacro = texmacro.substring(1);
   return unescape(macro2utf8[texmacro]);
 }
+
+function strip_errors() 
+{
+    errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
+    for (i = 0; i < errors.length; i++) {
+        children = errors[i].childNodes;
+        for (j = 0; j < children.length; j++) {
+            unlocked.insertBefore(children[j],errors[i]);
+	}
+        unlocked.removeChild(errors[i]);
+    }
+}
  
 function keypress(e)
 {
    if (!e) e= event;
    pressmesg('keypress',e);
    var s = string_of_key(e.charCode);
+   strip_errors();
    if (s == " ") {
 	j = getCursorPos();
 	i = unlocked.innerHTML.lastIndexOf('\\',j);
@@ -512,24 +535,31 @@ function advanceForm1()
 {
 	processor = function(xml) {
 		if (is_defined(xml)) {
+                        parsed = xml.getElementsByTagName("parsed")[0];
+                        if (is_defined(parsed)) {
 			// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-			parsed = xml.getElementsByTagName("parsed")[0];
-			len = parseInt(parsed.getAttribute("length"));
-	                // len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.html_to_matita();
-			parsedtxt = parsed.childNodes[0].nodeValue;
-			//parsedtxt = unescaped.substr(0,len); 
-			unparsedtxt = unescaped.substr(len);
-			lockedbackup += parsedtxt;
-			locked.innerHTML = lockedbackup;
-			unlocked.innerHTML = unparsedtxt.matita_to_html();
-			// len1 = unlocked.innerHTML.length;
-			// len2 = len0 - len1;
-			len2 = parsedtxt.length;
-			metasenv = xml.getElementsByTagName("meta");
-	                populate_goalarray(metasenv);
-			statements = listcons(len2,statements);
-			unlocked.scrollIntoView(true);
+			    len = parseInt(parsed.getAttribute("length"));
+	                    // len0 = unlocked.innerHTML.length;
+			    unescaped = unlocked.innerHTML.html_to_matita();
+			    parsedtxt = parsed.childNodes[0].nodeValue;
+			    //parsedtxt = unescaped.substr(0,len); 
+			    unparsedtxt = unescaped.substr(len);
+			    lockedbackup += parsedtxt;
+			    locked.innerHTML = lockedbackup;
+			    unlocked.innerHTML = unparsedtxt.matita_to_html();
+			    // len1 = unlocked.innerHTML.length;
+			    // len2 = len0 - len1;
+			    len2 = parsedtxt.length;
+			    metasenv = xml.getElementsByTagName("meta");
+	                    populate_goalarray(metasenv);
+			    statements = listcons(len2,statements);
+			    unlocked.scrollIntoView(true);
+			}
+		        else {
+                            error = xml.getElementsByTagName("error")[0]; 
+			    unlocked.innerHTML = error.childNodes[0].nodeValue;
+			    // debug(xml.childNodes[0].nodeValue);
+			}
 		} else {
 			debug("advance failed");
 		}