More changes to matitaweb.css.

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index e87a19f520d3171f259a7428ad58d44dff52de01..81995bb803ed42d8579f05d07d773ca252844b62 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -11,31 +11,42 @@ var advanceButton;
 var retractButton;
 var cursorButton;
 var bottomButton;
+var dialogBox;
+var dialogTitle;
+var dialogContent;
 var metasenv = "";
 
 function initialize()
 {
-  locked = document.getElementById("locked");
-  unlocked = document.getElementById("unlocked");
-  workarea = document.getElementById("workarea");
-  scriptcell = document.getElementById("scriptcell");
-  goalcell = document.getElementById("goalcell");
-  goals = document.getElementById("goals");
-  goalview = document.getElementById("goalview");
-  filename = document.getElementById("filename");
-  logarea = document.getElementById("logarea");
-  advanceButton = document.getElementById("advance");
-  retractButton = document.getElementById("retract");
-  cursorButton = document.getElementById("cursor");
-  bottomButton = document.getElementById("bottom");
-
-  // hide sequent view at start
-  hideSequent();
+  if (readCookie("session") == null) {
+    window.location = "/login.html"
+  } else {
+    locked = document.getElementById("locked");
+    unlocked = document.getElementById("unlocked");
+    workarea = document.getElementById("workarea");
+    scriptcell = document.getElementById("scriptcell");
+    goalcell = document.getElementById("goalcell");
+    goals = document.getElementById("goals");
+    goalview = document.getElementById("goalview");
+    filename = document.getElementById("filename");
+    logarea = document.getElementById("logarea");
+    advanceButton = document.getElementById("advance");
+    retractButton = document.getElementById("retract");
+    cursorButton = document.getElementById("cursor");
+    bottomButton = document.getElementById("bottom");
+    dialogBox = document.getElementById("dialogBox");
+    dialogTitle = document.getElementById("dialogTitle");
+    dialogContent = document.getElementById("dialogContent");
+  
+    // hide sequent view at start
+    hideSequent();
+  }
 }
 
 function debug(txt)
 {
-        logarea.innerHTML = txt + "\n" + logarea.innerHTML;
+        // internet explorer (v.9) doesn't work with innerHTML
+        logarea.innerText = txt + "\n" + logarea.innerText;
 }
 
 function listhd(l)
@@ -194,6 +205,19 @@ function switch_goal(meta)
   }
 }
 
+String.prototype.sescape = function() {
+       var patt1 = /%/gi;
+       var patt2 = /=/gi;
+       var patt3 = /&/gi;
+       var patt4 = /\+/gi;
+       var result = this;
+       result = result.replace(patt1,"%25");
+       result = result.replace(patt2,"%3D");
+       result = result.replace(patt3,"%26");
+       result = result.replace(patt4,"%2B");
+       return (result);
+}
+
 String.prototype.unescapeHTML = function()
 {
        var patt1 = /<br(\/|)>/gi;
@@ -279,7 +303,8 @@ function callServer(servicename,processResponse,reqbody)
                        }
                } 
        };
-       req.open("POST", servicename); // + escape(unlocked.innerHTML), true); 
+       req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
+        req.setRequestHeader("Content-type","application/x-www-form-urlencoded");      
        if (reqbody) {
                req.send(reqbody); 
        } else {
@@ -312,7 +337,7 @@ function advanceForm1()
                resume();
        };
        pause();
-        callServer("advance",processor,unlocked.innerHTML.unescapeHTML());
+        callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
   
 }
 
@@ -340,7 +365,7 @@ function gotoBottom()
                 resume();
        };
        pause();
-       callServer("bottom",processor,unlocked.innerHTML.unescapeHTML());
+       callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
   
 }
 
@@ -380,7 +405,7 @@ function gotoPos(offset)
                }
        }
        pause();
-       callServer("advance",processor,unlocked.innerHTML.unescapeHTML());
+       callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
 }
 
 function retract()
@@ -414,12 +439,53 @@ function openFile()
        {
                if (is_defined(xml)) {  
                        locked.innerHTML = "";
-                       unlocked.innerHTML = xml.documentElement.firstChild.data;
+                       unlocked.innerHTML = xml.documentElement.textContent;
                } else {
                        debug("file open failed");
                }
        };
-       callServer("open?file=" + escape(filename.value),processor); 
+       callServer("open",processor,"file=" + escape(filename.value)); 
+}
+
+function showLibrary()
+{ 
+       var req = null; 
+        // pause();
+       if (window.XMLHttpRequest)
+       {
+               req = new XMLHttpRequest();
+       } 
+       else if (window.ActiveXObject) 
+       {
+               try {
+                               req = new ActiveXObject("Msxml2.XMLHTTP");
+               } catch (e)
+               {
+                       try {
+                               req = new ActiveXObject("Microsoft.XMLHTTP");
+                               } catch (e) {}
+               }
+       }
+       req.onreadystatechange = function()
+       { 
+
+               rs = req.readyState;
+
+               if(rs == 4)
+               {
+                       stat = req.status;
+                       stxt = req.statusText;
+                       if(stat == 200)
+                       {
+                         debug(req.responseText);
+                         showDialog("<H2>Library</H2>",req.responseText);
+                       } 
+               } 
+       };
+       req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
+        req.setRequestHeader("Content-type","application/x-www-form-urlencoded");      
+       req.send();
+  
 }
 
 var goalcell;
@@ -434,6 +500,12 @@ function showSequent() {
   workarea.appendChild(goalcell);
 }
 
+function showDialog(title,content) {
+  dialogTitle.innerHTML = title;
+  dialogContent.innerHTML = content;
+  dialogBox.style.display = "block";
+}
+
 function removeElement(id) {
   var element = document.getElementById(id);
   element.parentNode.removeChild(element);
@@ -484,3 +556,26 @@ function findNode(list, node, acc) {
 function test () {
   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 }
+
+function readCookie(name) {
+       var nameEQ = name + "=";
+       var ca = document.cookie.split(';');
+       for(var i=0;i < ca.length;i++) {
+               var c = ca[i];
+               while (c.charAt(0)==' ') c = c.substring(1,c.length);
+               if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
+       }
+       return null;
+}
+
+function delete_cookie ( cookie_name )
+{
+  var cookie_date = new Date();  // current date & time
+  cookie_date.setTime ( cookie_date.getTime() - 1 );
+  document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
+}
+
+function delete_session()
+{
+       delete_cookie("session");
+}