Matitaweb: added a titlebar to the GUI.

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index e4fbe56334a9f3729e0d10c6ba05d089af8ffce3..f0563928234812f20f980c467fc9b671784a1e6a 100644 (file)
--- 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)
@@ -690,7 +698,7 @@ 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)
@@ -822,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?")) {
@@ -831,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); }
                  }