X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=fb6c0869da5b9c6afac25648187987195215b07c;hb=d8bc6fd4ab18f2995624c75e2889318237e9c17f;hp=8b607e21adcb897cebea009b3bdcc98075bb2d69;hpb=66cd2dbc1838b93c9d89511b4fed5848e2c6d65d;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 8b607e21a..fb6c0869d 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -108,7 +108,7 @@ function suppressdefault(e,flag)
    return !flag;
 }
 
-function restoreSelection() {
+function restoreSelection(adjust) {
     unlocked.focus();
     if (savedRange != null) {
         if (window.getSelection)//non IE and there is already a selection
@@ -117,7 +117,7 @@ function restoreSelection() {
             if (s.rangeCount > 0) 
                 s.removeAllRanges();
 	    range = document.createRange();
-	    range.setStart(savedsc,savedso);
+	    range.setStart(savedsc,savedso + adjust);
 	    range.collapse(true);
             s.addRange(range);
         }
@@ -133,6 +133,12 @@ function restoreSelection() {
                 }
     }
 }
+
+function lookup_tex(texmacro)
+{
+  texmacro = texmacro.substring(1);
+  return unescape(macro2utf8[texmacro]);
+}
  
 function keypress(e)
 {
@@ -146,13 +152,17 @@ function keypress(e)
 	  match = unlocked.innerHTML.substring(i,j);
 	  pre = unlocked.innerHTML.substring(0,i);
 	  post = unlocked.innerHTML.substring(j);
-	  if (match == '\\to') {
-             unlocked.innerHTML = pre + "-> " + post;
-             restoreSelection(); 
+	  
+	  sym = lookup_tex(match);
+	  if (typeof sym != "undefined") {
+	     len1 = unlocked.innerText.length;
+             unlocked.innerHTML = pre + sym + post;
+	     len2 = unlocked.innerText.length;
+             restoreSelection(len2 - len1); 
  	     return suppressdefault(e,true);
 	  }
 	  else {
-             restoreSelection(); 
+             // restoreSelection(0); 
 	     return suppressdefault(e,false);
 	  }
 	}
@@ -339,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));
 }
 
@@ -439,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");
@@ -458,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());
   
 }
 
@@ -467,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");
@@ -486,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());
   
 }
 
@@ -498,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");
@@ -526,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()
@@ -574,7 +607,9 @@ function retrieveFile(thefile)
 	{
 	        if (is_defined(xml)) {	
 	        	locked.innerHTML = "";
-	                unlocked.innerHTML = xml.documentElement.textContent;
+			debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
+	                unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
+
 		} else {
 			debug("file open failed");
 		}