X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=cd1e624e1fba6664db95a222bdfd426a593e00ae;hb=0aa993bb1d23567612aa5d63fab74ef6fb918c0d;hp=c98937735770f2023f9a2ff585d8510962f8e788;hpb=5fbe7da7019bda8fead167c8b1da1b06625551b3;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index c98937735..cd1e624e1 100644
--- 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";