X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=48acfe13e223a0118b03b5d96ddc7b1a36250513;hb=b352c0b72bb62f7b4a44952aebc01f405f6af817;hp=07dbb06f68c7ce6717b442fbc1c716551caff28f;hpb=acf77bb24694158a57444c7f32da46ceac8b30c4;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 07dbb06f6..48acfe13e 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -178,7 +178,8 @@ function debug(txt) // internet explorer (v.9) doesn't work with innerHTML // but google chrome's innerText is, in a sense, "write only" // what should we do? - logarea.innerText = txt + "\n" + logarea.innerText; + // logarea.innerText = txt + "\n" + logarea.innerText; + logarea.innerHTML = txt; // + "\n" + logarea.innerText; } function listhd(l) @@ -507,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; @@ -611,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"); } @@ -626,8 +629,11 @@ function retrieveFile(thefile) if (is_defined(xml)) { lockedbackup = "" locked.innerHTML = lockedbackup; - debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); - unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; + // code originally used in google chrome (problems with mozilla) + // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); + // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; + debug(xml.childNodes[0].textContent); + unlocked.innerHTML = xml.childNodes[0].textContent; } else { debug("file open failed"); @@ -638,7 +644,7 @@ function retrieveFile(thefile) callServer("open",processor,"file=" + escape(thefile)); } -function showLibrary() +function showLibrary(title,callback) { var req = null; // pause(); @@ -669,7 +675,7 @@ function showLibrary() if(stat == 200) { debug(req.responseText); - showDialog("