X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=81995bb803ed42d8579f05d07d773ca252844b62;hb=bb9c48af6f729b0616a0fc5f1fd9037d4c3f2c89;hp=21478e4634c69e13b8ac42fb8f728e943cd8f5ad;hpb=07c264b088aa018552a810ff365b0d889fb0fd5c;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 21478e463..81995bb80 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -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("<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() {
@@ -457,10 +500,10 @@ 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) {