]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitaweb.js
Show library test 1.
[helm.git] / matitaB / matita / matitaweb.js
index 21478e4634c69e13b8ac42fb8f728e943cd8f5ad..a5bf84adcd4610afdd532a35767654ec81434671 100644 (file)
@@ -13,6 +13,7 @@ var cursorButton;
 var bottomButton;
 var dialogBox;
 var dialogTitle;
+var dialogContent;
 var metasenv = "";
 
 function initialize()
@@ -35,6 +36,7 @@ function initialize()
     bottomButton = document.getElementById("bottom");
     dialogBox = document.getElementById("dialogBox");
     dialogTitle = document.getElementById("dialogTitle");
+    dialogContent = document.getElementById("dialogContent");
   
     // hide sequent view at start
     hideSequent();
@@ -445,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("Library",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() {
@@ -457,10 +500,11 @@ function showSequent() {
   workarea.appendChild(goalcell);
 }
 
-function showDialog(title) {
+function showDialog(title,content) {
 
+  dialogTitle.innerHTML = title;
+  dialogContent.innerHTML = content;
   dialogBox.style.display = "block";
-  dialogTitle.innerHTML = title; 
 }
 
 function removeElement(id) {