Matitaweb:

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index c98937735770f2023f9a2ff585d8510962f8e788..cd1e624e1fba6664db95a222bdfd426a593e00ae 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -85,9 +85,33 @@ function initialize()
 
     // initialize keyboard events in the unlocked script
     init_keyboard(unlocked);
+
+    init_autotraces();
+
   }
 }
 
+function init_autotraces() {
+    $("#unlocked .autotactic").tooltip({ 
+      delay: 0, 
+      showURL: false, 
+      bodyHandler: function() { 
+        return (trace_of($(this)[0])); 
+      }
+    });
+    $("#locked .autotactic").tooltip({ 
+      delay: 0, 
+      showURL: false, 
+      bodyHandler: function() { 
+        return (trace_of($(this)[0]));
+      }
+    });
+}
+
+function trace_of(node) {
+  return text_of_html(filterByClass(node.childNodes,"autotrace")[0]);
+}
+
 function changeFile(name) {
     current_fname = name;
     matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
@@ -196,7 +220,7 @@ function strip_tags(tagname,classname)
             tags[i].parentNode.insertBefore(children[j],tags[i]);
        }
     }
-    for (;tags.length > 0;) {
+    while (tags.length > 0) {
       tags[0].parentNode.removeChild(tags[0]);
     }
 }
@@ -214,9 +238,9 @@ function keypress(e)
    strip_tags("span","error");
    if (s == " ") {
        j = getCursorPos();
-       i = unlocked.innerHTML.lastIndexOf('\\',j);
+       i = unlocked.innerHTML.html_to_matita().lastIndexOf('\\',j);
                if (i >= 0) {
-         match = unlocked.innerHTML.substring(i,j);
+         match = unlocked.innerHTML.html_to_matita().substring(i,j);
          sym = unescape_html(lookup_tex(match));
          if (sym != "undefined") {
              if (window.getSelection) { // non IE
@@ -575,6 +599,7 @@ function advanceForm1()
                            var len2 = parsedtxt.length;
                            var metasenv = xml.getElementsByTagName("meta");
                            populate_goalarray(metasenv);
+                           init_autotraces();
                            statements = listcons(len2,statements);
                            unlocked.scrollIntoView(true);
                        }
@@ -674,6 +699,7 @@ function gotoBottom()
                          // len1 = unlocked.innerHTML.length;
                          len2 = parsedtxt.length;
                          metasenv = xml.getElementsByTagName("meta");
+                         init_autotraces();
                          populate_goalarray(metasenv);
                          if (len2 > 0)
                            statements = listcons(len2,statements);
@@ -708,6 +734,7 @@ function gotoTop()
                        unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
                        lockedbackup = "";
                         locked.innerHTML = lockedbackup;
+                       init_autotraces();
                         hideSequent();
                         unlocked.scrollIntoView(true);
                } else {
@@ -744,12 +771,14 @@ function gotoPos(offset)
                        unlocked.scrollIntoView(true);
                        // la populate non andrebbe fatta a ogni passo
                        if (offset <= len) {
+                               init_autotraces();
                                populate_goalarray(metasenv);
                                resume();
                        } else {
                                gotoPos(offset - len);
                        }
                } else {
+                       init_autotraces();
                        unlocked.scrollIntoView(true);
                        populate_goalarray(metasenv);
                        resume();
@@ -778,6 +807,7 @@ function retract()
                         locked.innerHTML = lockedbackup;
                        unlocked.innerHTML = statement + unlocked.innerHTML;
                        metasenv = xml.getElementsByTagName("meta");
+                       init_autotraces();
                         populate_goalarray(metasenv);
                         unlocked.scrollIntoView(true);
                } else {
@@ -823,6 +853,7 @@ function retrieveFile(thefile)
                         } else {
                           unlocked.innerHTML = xml.childNodes[0].textContent;
                         }
+                       init_autotraces();
 
                } else {
                        debug("file open failed");
@@ -1049,8 +1080,8 @@ function showDialog(title,content,callback) {
   $('#mask').css({'width':maskWidth,'height':maskHeight});
   
   //transition effect          
-  $('#mask').fadeIn(1000);     
-  $('#mask').fadeTo("slow",0.8);       
+  $('#mask').fadeIn(100);      
+  $('#mask').fadeTo(200,0.8);  
   
   //Get the window height and width
   var winH = $(window).height();
@@ -1061,7 +1092,7 @@ function showDialog(title,content,callback) {
   $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
   
   //transition effect
-  $('#dialogBox').fadeIn(2000); 
+  $('#dialogBox').fadeIn(200); 
 
   dialogBox.style.display = "block";
 }
@@ -1117,7 +1148,7 @@ function findNode(list, node, acc) {
     dup = list[i].cloneNode(true);
     sandbox.appendChild(dup);
 //    debug("fail " + i + ": " + sandbox.innerHTML);
-    acc += sandbox.innerHTML.length;
+    acc += sandbox.innerHTML.html_to_matita().length;
     sandbox.removeChild(dup);
   }
   throw "not found";