X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=86481a1ed15417a77dc3cdbc732cc02d17ceb7ee;hb=6c146035564b39f54a3c919135f179cec349c284;hp=07dbb06f68c7ce6717b442fbc1c716551caff28f;hpb=e0433942a61cfe8b43b68a81efa7d7d68abe3c5a;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 07dbb06f6..86481a1ed 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.innerHTML;
 }
 
 function listhd(l)
@@ -626,8 +627,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");