Matitaweb: several improvements to svn interface.

[helm.git] / matitaB / matita / matitaweb.js

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 349097719c405584c88f49a166e99c6ebac399e2..e4fbe56334a9f3729e0d10c6ba05d089af8ffce3 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -392,12 +392,14 @@ String.prototype.html_to_matita = function()
        var patt3 = />/gi
        var patt4 = /</gi;
        var patt5 = />/gi;
+       var patt6 = / /gi;
        var result = this;
        result = result.replace(patt1,"\n");
        result = result.replace(patt2,"\005");
        result = result.replace(patt3,"\006");
        result = result.replace(patt4,"<");
        result = result.replace(patt5,">");
+       result = result.replace(patt6," ");
        return (unescape(result));
 }
 
@@ -695,7 +697,11 @@ function retrieveFile(thefile)
                        // 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;
+                        if (document.all) { // IE
+                          unlocked.innerHTML = xml.childNodes[0].text;
+                        } else {
+                          unlocked.innerHTML = xml.childNodes[0].textContent;
+                        }
 
                } else {
                        debug("file open failed");
@@ -870,9 +876,11 @@ function commitAll()
 {
        processor = function(xml) {
                if (is_defined(xml)) {
-                       debug("commit succeeded(?)");
+                        debug(xml.getElementsByTagName("details")[0].textContent);
+                       alert("Commit executed: see details in the log.\n\n" +
+                              "NOTICE: this message does NOT imply (yet) that the commit was successful.");
                } else {
-                       debug("commit failed!");
+                       alert("Commit failed!");
                }
                resume();
        };
@@ -884,9 +892,11 @@ function updateAll()
 {
        processor = function(xml) {
                if (is_defined(xml)) {
-                       debug("update succeeded(?)");
+                       alert("Update executed.\n\n" +
+                              "Details:\n" +
+                              xml.getElementsByTagName("details")[0].textContent);
                } else {
-                       debug("update failed!");
+                       alert("Update failed!");
                }
                resume();
        };