]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitaweb.js
More changes to matitaweb.css.
[helm.git] / matitaB / matita / matitaweb.js
index 423eda674bbd1ed06c54d379dd65e56b5fb78f24..81995bb803ed42d8579f05d07d773ca252844b62 100644 (file)
@@ -11,6 +11,9 @@ var advanceButton;
 var retractButton;
 var cursorButton;
 var bottomButton;
+var dialogBox;
+var dialogTitle;
+var dialogContent;
 var metasenv = "";
 
 function initialize()
@@ -31,6 +34,9 @@ function initialize()
     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();
@@ -441,6 +447,47 @@ function openFile()
        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;
 
 function hideSequent() {
@@ -453,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);