From: Wilmer Ricciotti Date: Wed, 22 Jun 2011 12:25:51 +0000 (+0000) Subject: First attempt at dialog boxes. X-Git-Tag: make_still_working~2414 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2caa495ad67af93b2b5a2b6b54c96745ff5e8a7;p=helm.git First attempt at dialog boxes. --- diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 223aefa3e..415a37758 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -1,9 +1,8 @@ - - - + + @@ -24,6 +23,7 @@

+ @@ -55,5 +55,10 @@ + + diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css new file mode 100644 index 000000000..91e5b5479 --- /dev/null +++ b/matitaB/matita/matitaweb.css @@ -0,0 +1,19 @@ +div.dialog { + position:absolute; + top: 50%; + left: 50%; + width:400px; + height:300px; + margin-top: -150px; /*set to a negative number 1/2 of your height*/ + margin-left: -200px; /*set to a negative number 1/2 of your width*/ + border: 1px solid #ccc; + background-color: #f3f3f3; +} + +div.scroll { + border: 1px; + border-style:solid; + height:100%; + width:100%; + overflow:auto; +} diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 423eda674..f66223c6e 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -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);