Opening scripts using the Library dialog (try 1).

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 81995bb803ed42d8579f05d07d773ca252844b62..e785011b5d5a2988a880b1a75540e9adeeed6459 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -447,6 +447,21 @@ function openFile()
        callServer("open",processor,"file=" + escape(filename.value)); 
 }
 
+function retrieveFile(thefile)
+{ 
+       processor = function(xml)
+       {
+               if (is_defined(xml)) {  
+                       locked.innerHTML = "";
+                       unlocked.innerHTML = xml.documentElement.textContent;
+               } else {
+                       debug("file open failed");
+               }
+       };
+       dialogBox.style.display = "none";
+       callServer("open",processor,"file=" + escape(thefile); 
+}
+
 function showLibrary()
 { 
        var req = null;