Matitaweb:

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 44fd608a1bbf7b099f495a2789cb6a0242fb1af9..c98937735770f2023f9a2ff585d8510962f8e788 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -34,10 +34,10 @@ function unescape_html(s)
   return text_of_html(u)
 }
 
-function filterByClass (elements,class){
+function filterByClass (elements,cname){
   var itemsfound = new Array;
   for(var i=0;i<elements.length;i++){
-    if(elements[i].className == class){
+    if(elements[i].className == cname){
       itemsfound.push(elements[i]);
     }
   }
@@ -184,16 +184,26 @@ function lookup_tex(texmacro)
   return unescape(macro2utf8[texmacro]);
 }
 
-function strip_errors() 
+function strip_tags(tagname,classname) 
 {
-    errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
-    for (i = 0; i < errors.length; i++) {
-        children = errors[i].childNodes;
+    var tags = unlocked.getElementsByTagName(tagname);
+    if (is_defined(classname)) {
+       tags = filterByClass(tags,classname);
+    }
+    for (i = 0; i < tags.length; i++) {
+        var children = tags[i].childNodes;
         for (j = 0; j < children.length; j++) {
-            unlocked.insertBefore(children[j],errors[i]);
+            tags[i].parentNode.insertBefore(children[j],tags[i]);
        }
-        unlocked.removeChild(errors[i]);
     }
+    for (;tags.length > 0;) {
+      tags[0].parentNode.removeChild(tags[0]);
+    }
+}
+
+function strip_interpr() {
+       strip_tags("A");
+       alert("strip_interpr ended");
 }
  
 function keypress(e)
@@ -201,7 +211,7 @@ function keypress(e)
    if (!e) e= event;
    pressmesg('keypress',e);
    var s = string_of_key(e.charCode);
-   strip_errors();
+   strip_tags("span","error");
    if (s == " ") {
        j = getCursorPos();
        i = unlocked.innerHTML.lastIndexOf('\\',j);
@@ -623,6 +633,8 @@ function advanceForm1()
                            disambcell.appendChild(okbutton);
                            disambcell.appendChild(cancelbutton);
 
+                           disable_toparea();
+
                            matita.disambMode = true;
                            updateSide();
                        }
@@ -816,7 +828,7 @@ function retrieveFile(thefile)
                        debug("file open failed");
                }
        };
-       dialogBox.style.display = "none";
+       abortDialog();
        callServer("open",processor,"file=" + escape(thefile)); 
 }
 
@@ -901,7 +913,7 @@ function openDialog()
 function saveDialog()
 {  
        callback = function (fname) { 
-         dialogBox.style.display = "none";
+         abortDialog();
           saveFile(fname,
                   (locked.innerHTML.html_to_matita()).sescape(),
                   (unlocked.innerHTML.html_to_matita()).sescape(),
@@ -913,7 +925,7 @@ function saveDialog()
 function newDialog()
 {
        callback = function (fname) { 
-         dialogBox.style.display = "none";
+         abortDialog();
          saveFile(fname,"","",false,newDialog,true);
        };
        showLibrary("Create new file", callback, newDialog);
@@ -1028,15 +1040,34 @@ function showDialog(title,content,callback) {
   dialogTitle.innerHTML = title;
   dialogContent.innerHTML = content;
   dialogBox.callback = callback;
-  dialogBox.style.display = "block";
-}
 
-function showDisamb(content) {
-  disambContent.innerHTML = content;
-  disambBox.style.display = "block";
+  //Get the screen height and width
+  var maskHeight = $(document).height();
+  var maskWidth = $(window).width();
+  
+  //Set heigth and width to mask to fill up the whole screen
+  $('#mask').css({'width':maskWidth,'height':maskHeight});
+  
+  //transition effect          
+  $('#mask').fadeIn(1000);     
+  $('#mask').fadeTo("slow",0.8);       
+  
+  //Get the window height and width
+  var winH = $(window).height();
+  var winW = $(window).width();
+  
+  //Set the popup window to center
+  $('#dialogBox').css('top',  winH/2-$('#dialogBox').height()/2);
+  $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
+  
+  //transition effect
+  $('#dialogBox').fadeIn(2000); 
+
+  dialogBox.style.display = "block";
 }
 
 function abortDialog(dialog) {
+  $('#mask').hide();
   dialogBox.style.display = "none";
 }
 
@@ -1108,6 +1139,7 @@ function get_checked_index(name) {
 
 function cancel_disambiguate() {
        matita.disambMode = false;
+       $('#whitemask').hide();
        updateSide();
 }
 
@@ -1134,6 +1166,7 @@ function do_disambiguate() {
            unlocked.innerHTML = pre + mid + post;
 
            matita.disambMode = false;
+           $('#whitemask').hide();
            updateSide();
        }
 }
@@ -1160,3 +1193,12 @@ function delete_session()
 {
        delete_cookie("session");
 }
+
+function disable_toparea() {
+       var offset = $('#toparea').offset();
+        $('#whitemask').css('top',offset.top);
+        $('#whitemask').css('left',offset.left);
+        $('#whitemask').css('width',$('#toparea').outerWidth() + "px");
+        $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
+       $('#whitemask').fadeTo('fast',0.7);
+}