]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitaweb.js
First attempt at dialog boxes.
[helm.git] / matitaB / matita / matitaweb.js
index 423eda674bbd1ed06c54d379dd65e56b5fb78f24..f66223c6e5d097ad76e7758e58798bd6b203d53f 100644 (file)
@@ -11,6 +11,8 @@ var advanceButton;
 var retractButton;
 var cursorButton;
 var bottomButton;
+var dialogBox;
+var dialogTitle;
 var metasenv = "";
 
 function initialize()
@@ -31,6 +33,8 @@ function initialize()
     retractButton = document.getElementById("retract");
     cursorButton = document.getElementById("cursor");
     bottomButton = document.getElementById("bottom");
+    dialogBox = document.getElementById("dialogBox");
+    dialogTitle = document.getElementById("dialogTitle");
   
     // hide sequent view at start
     hideSequent();
@@ -453,6 +457,12 @@ function showSequent() {
   workarea.appendChild(goalcell);
 }
 
+function showDialog(title) {
+
+  dialogBox.display = "block";
+  dialogTitle.innerHTML = title; 
+}
+
 function removeElement(id) {
   var element = document.getElementById(id);
   element.parentNode.removeChild(element);