return (result);
}
-String.prototype.unescapeHTML = function()
+String.prototype.html_to_matita = function()
{
var patt1 = /<br(\/|)>/gi;
- var patt2 = /</gi;
- var patt3 = />/gi;
+ var patt2 = /</gi
+ var patt3 = />/gi
+ var patt4 = /</gi;
+ var patt5 = />/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,"<");
+ result = result.replace(patt2,">");
+ result = result.replace(patt3,"<");
+ result = result.replace(patt4,">");
return (unescape(result));
}
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");
resume();
};
pause();
- callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+ callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
}
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");
resume();
};
pause();
- callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+ callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
}
}
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");
}
}
pause();
- callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+ callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
}
function retract()
{
if (is_defined(xml)) {
locked.innerHTML = "";
+ debug(xml.documentElement.textContent);
unlocked.innerHTML = xml.documentElement.textContent;
} else {
debug("file open failed");