From: matitaweb Date: Wed, 7 Sep 2011 13:47:44 +0000 (+0000) Subject: Changed behavior in matitaweb.js, function retrieveFile (it is now X-Git-Tag: make_still_working~2312 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c146035564b39f54a3c919135f179cec349c284;p=helm.git Changed behavior in matitaweb.js, function retrieveFile (it is now compatible with Firefox, hopefully). --- diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 5abb8ad07..61b2dc547 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -269,7 +269,7 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (try MatitaAuthentication.add_user uid userpw; (* env#set_output_header_field "Location" "/index.html" *) - cgi#outchannel#output_string + cgi#out_channel#output_string ("" ^ "Redirecting to login page...") with @@ -309,7 +309,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = env#set_output_header_field "Set-Cookie" ("session=" ^ (Uuidm.to_string sid)); (* env#set_output_header_field "Location" "/index.html" *) - cgi#outchannel#output_string + cgi#out_channel#output_string ("" ^ "Redirecting to Matita page...") end 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"); diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf index 8764b1738..10e9c55dc 100644 --- a/matitaB/matita/netplex.conf +++ b/matitaB/matita/netplex.conf @@ -27,7 +27,7 @@ netplex { path = "/"; service { type = "file"; - docroot = "/home/barolo/matitaB/matita"; + docroot = "/home/matitaweb/matita/matita"; media_types_file = "/etc/mime.types"; enable_listings = true; }