X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=48acfe13e223a0118b03b5d96ddc7b1a36250513;hb=b352c0b72bb62f7b4a44952aebc01f405f6af817;hp=86481a1ed15417a77dc3cdbc732cc02d17ceb7ee;hpb=6c146035564b39f54a3c919135f179cec349c284;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 86481a1ed..48acfe13e 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -179,7 +179,7 @@ function debug(txt) // but google chrome's innerText is, in a sense, "write only" // what should we do? // logarea.innerText = txt + "\n" + logarea.innerText; - logarea.innerHTML = txt + "\n" + logarea.innerHTML; + logarea.innerHTML = txt; // + "\n" + logarea.innerText; } function listhd(l) @@ -508,7 +508,9 @@ function gotoBottom() if (len > 0) { // len0 = unlocked.innerHTML.length; unescaped = unlocked.innerHTML.html_to_matita(); - parsedtxt = parsed.childNodes[0].nodeValue; + // not working in mozilla + // parsedtxt = parsed.childNodes[0].nodeValue; + parsedtxt = parsed.childNodes[0].wholeText; //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); lockedbackup += parsedtxt; @@ -612,7 +614,7 @@ function openFile() if (is_defined(xml)) { lockedbackup = ""; locked.innerHTML = lockedbackup; - unlocked.innerHTML = xml.documentElement.textContent; + unlocked.innerHTML = xml.documentElement.wholeText; } else { debug("file open failed"); } @@ -642,7 +644,7 @@ function retrieveFile(thefile) callServer("open",processor,"file=" + escape(thefile)); } -function showLibrary() +function showLibrary(title,callback) { var req = null; // pause(); @@ -673,7 +675,7 @@ function showLibrary() if(stat == 200) { debug(req.responseText); - showDialog("