X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=04787ce77d3961a0919ecf9faf0e7ba24ed64ce0;hb=dee464f8cd331524663167659d1fad01e558d4e1;hp=e4b0efdba98cc4f72e3d9b22c8fca2519fc8a398;hpb=d83fa3d6e3604bcc596840219f3998d795630d66;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index e4b0efdba..04787ce77 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -349,15 +349,33 @@ String.prototype.sescape = function() {
 	return (result);
 }
 
-String.prototype.unescapeHTML = function()
+String.prototype.html_to_matita = function()
 {
 	var patt1 = /<br(\/|)>/gi;
-	var patt2 = /&lt;/gi;
-	var patt3 = /&gt;/gi;
+	var patt2 = /</gi
+	var patt3 = />/gi
+	var patt4 = /&lt;/gi;
+	var patt5 = /&gt;/gi;
 	var result = this;
 	result = result.replace(patt1,"\n");
-	result = result.replace(patt2,"<");
-	result = result.replace(patt3,">");
+	result = result.replace(patt2,"\005");
+	result = result.replace(patt3,"\006");
+	result = result.replace(patt4,"<");
+	result = result.replace(patt5,">");
+	return (unescape(result));
+}
+
+String.prototype.matita_to_html = function()
+{
+	var patt1 = /</gi
+	var patt2 = />/gi
+	var patt3 = /\005/gi;
+	var patt4 = /\006/gi;
+	var result = this;
+	result = result.replace(patt1,"&lt;");
+	result = result.replace(patt2,"&gt;");
+	result = result.replace(patt3,"<");
+	result = result.replace(patt4,">");
 	return (unescape(result));
 }
 
@@ -449,13 +467,15 @@ function advanceForm1()
 	processor = function(xml) {
 		if (is_defined(xml)) {
 			// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -468,7 +488,7 @@ function advanceForm1()
 		resume();
 	};
 	pause();
-        callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+        callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
   
 }
 
@@ -477,13 +497,15 @@ function gotoBottom()
 	processor = function(xml) {
 		if (is_defined(xml)) {
 			// debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -496,7 +518,7 @@ function gotoBottom()
                 resume();
 	};
 	pause();
-	callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+	callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
   
 }
 
@@ -508,14 +530,15 @@ function gotoPos(offset)
         }
 	processor = function(xml) {
 		if (is_defined(xml)) {
-			// debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -536,7 +559,7 @@ function gotoPos(offset)
 		}
 	}
 	pause();
-	callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+	callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 }
 
 function retract()
@@ -584,6 +607,7 @@ function retrieveFile(thefile)
 	{
 	        if (is_defined(xml)) {	
 	        	locked.innerHTML = "";
+			debug(xml.documentElement.textContent);
 	                unlocked.innerHTML = xml.documentElement.textContent;
 		} else {
 			debug("file open failed");