X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=f0563928234812f20f980c467fc9b671784a1e6a;hb=0fdf8cd395b21ec003569383aee1449a6fe4b35a;hp=349097719c405584c88f49a166e99c6ebac399e2;hpb=92a81bb9f7e51807585feb00f102b1f02d6cf1d3;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 349097719..f05639282 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -38,6 +38,7 @@ function initialize()
   if (readCookie("session") == null) {
     window.location = "/login.html"
   } else {
+    matitaTitle = document.getElementById("matitaTitle");
     locked = document.getElementById("locked");
     unlocked = document.getElementById("unlocked");
     workarea = document.getElementById("workarea");
@@ -54,6 +55,8 @@ function initialize()
     dialogBox = document.getElementById("dialogBox");
     dialogTitle = document.getElementById("dialogTitle");
     dialogContent = document.getElementById("dialogContent");
+
+    changeFile("test.ma");
   
     // hide sequent view at start
     hideSequent();
@@ -63,6 +66,11 @@ function initialize()
   }
 }
 
+function changeFile(name) {
+    current_fname = name;
+    matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+}
+
 function init_keyboard(target)
 {
     if (target.addEventListener)
@@ -392,12 +400,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));
 }
 
@@ -688,14 +698,18 @@ function retrieveFile(thefile)
 	processor = function(xml)
 	{
 	        if (is_defined(xml)) {	
-	                current_fname = thefile;
+	                changeFile(thefile);
 	        	lockedbackup = ""
 			locked.innerHTML = lockedbackup;
                         // 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;
+                        if (document.all) { // IE
+                          unlocked.innerHTML = xml.childNodes[0].text;
+                        } else {
+                          unlocked.innerHTML = xml.childNodes[0].textContent;
+                        }
 
 		} else {
 			debug("file open failed");
@@ -816,7 +830,6 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
 	    // when force is true, reloadDialog is not needed 
         }
 	processor = function(xml) {
-	        current_fname = fname;
 		if (is_defined(xml)) {
 		  if (xml.childNodes[0].textContent != "ok") {
                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
@@ -825,7 +838,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
                       reloadDialog();
 		    }
 		  } else {
-  	            current_fname = fname;
+  	            changeFile(fname);
 	            debug("file saved!");
                     if (reloadFile) { retrieveFile(fname); }
 		  }
@@ -870,9 +883,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 +899,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();
 	};