]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/html/matitaweb.js
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Hyperlink support.
[helm.git] / matitaB / matita / html / matitaweb.js
diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 20d0fec43dbcf9557da473af7fae857413b3d60e..6661cd04ad5959b28ae8f6d8ff49341dc441eeb7 100644 (file)
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -86,11 +86,34 @@ function initialize()
     // initialize keyboard events in the unlocked script
     init_keyboard(unlocked);
 
+    init_hyperlinks();
     init_autotraces();
 
   }
 }
 
+function go_hyperlink(atag) {
+  var uri = atag.attr("href");
+  var mybaseuri = uri.substring(0,uri.lastIndexOf('/'));
+  var id = uri.substring(uri.lastIndexOf('/')+1,uri.lastIndexOf('.'));
+  // 12 = position of the second '/' in mybaseuri (to strip off "cic:/matita/")
+  var thefile = mybaseuri.substring(12) + ".ma";
+  if (uri != "cic:/fakeuri.def(1)") {
+     if (mybaseuri == baseuri) {
+        $('#'+id)[0].scrollIntoView(true);
+     } else {
+       go_external_hyperlink(mybaseuri,thefile,id);
+     }
+  }
+  return false;
+}
+
+function init_hyperlinks() {
+  $("#unlocked a").click(function () { return go_hyperlink($(this))});
+  $("#locked a").click(function () { return go_hyperlink($(this))});
+  $("#goalview a").click(function () { return go_hyperlink($(this))});
+}
+
 function init_autotraces() {
     $("#unlocked .autotactic").tooltip({ 
       delay: 0, 
@@ -115,6 +138,7 @@ function trace_of(node) {
 function changeFile(name) {
     current_fname = name;
     matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+    baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
 }
 
 function init_keyboard(target)
@@ -227,8 +251,14 @@ function strip_tags(tagname,classname)
 }
 
 function strip_interpr() {
+       pause();
        strip_tags("A");
-       alert("strip_interpr ended");
+       resume();
+       // alert("strip_interpr ended");
+}
+
+function strip_anchors() {
+       strip_tags("INPUT","anchor");
 }
  
 function keypress(e)
@@ -284,8 +314,8 @@ function debug(txt)
 }
 
 function showLog() {
-  logWin = window.open( "", "Matita Log",
-     "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
+  var logWin = window.open( "", "Matita Log",
+     "width=600,height=450,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
   logWin.document.write('<html><head><title>Matita Log' + '</title></head>');  
   logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
     logtxt + '</textarea></body></html>');
@@ -675,6 +705,7 @@ function advanceForm1()
                if (is_defined(xml)) {
                    advOneStep(xml);
                     populate_goalarray(metasenv);
+                   init_hyperlinks();
                    init_autotraces();
                } else {
                        debug("advance failed");
@@ -901,6 +932,7 @@ function gotoBottom()
                        }
                        unlocked.scrollIntoView(true);
                        metasenv = xml.getElementsByTagName("meta");
+                       init_hyperlinks();
                        init_autotraces();
                        populate_goalarray(metasenv);
 
@@ -1007,8 +1039,10 @@ function gotoTop()
                        unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
                        lockedbackup = "";
                         locked.innerHTML = lockedbackup;
+                       init_hyperlinks();
                        init_autotraces();
                         hideSequent();
+                       strip_anchors();
                         unlocked.scrollIntoView(true);
                } else {
                        debug("goto top failed");
@@ -1049,6 +1083,7 @@ function gotoPos(offset)
                        */
                        var len = advOneStep(xml);
                        if (offset <= len) {
+                               init_hyperlinks();
                                init_autotraces();
                                populate_goalarray(metasenv);
                                resume();
@@ -1056,11 +1091,13 @@ function gotoPos(offset)
                                gotoPos(offset - len);
                        }
                    } catch (er) {
+                       init_hyperlinks();
                        init_autotraces();
                        populate_goalarray(metasenv);
                        resume();
                    }
                } else {
+                       init_hyperlinks();
                        init_autotraces();
                        unlocked.scrollIntoView(true);
                        populate_goalarray(metasenv);
@@ -1090,8 +1127,10 @@ function retract()
                         locked.innerHTML = lockedbackup;
                        unlocked.innerHTML = statement + unlocked.innerHTML;
                        metasenv = xml.getElementsByTagName("meta");
-                       init_autotraces();
                         populate_goalarray(metasenv);
+                       init_hyperlinks();
+                       init_autotraces();
+                       strip_anchors();
                         unlocked.scrollIntoView(true);
                } else {
                        debug("retract failed");
@@ -1110,6 +1149,7 @@ function openFile()
                        lockedbackup = "";
                        locked.innerHTML = lockedbackup;
                        unlocked.innerHTML = xml.documentElement.wholeText;
+                       strip_anchors();
                } else {
                        debug("file open failed");
                }
@@ -1137,6 +1177,8 @@ function retrieveFile(thefile)
                         } else {
                           unlocked.innerHTML = xml.childNodes[0].textContent;
                         }
+                       strip_anchors();
+                       init_hyperlinks();
                        init_autotraces();
 
                } else {
@@ -1147,6 +1189,59 @@ function retrieveFile(thefile)
        callServer("open",processor,"file=" + escape(thefile)); 
 }
 
+function go_external_hyperlink(uri,thefile,id)
+{ 
+       var docWin = createDocWin(uri);
+       processor = function(xml)
+       {
+               if (is_defined(xml)) {  
+                        // code originally used in google chrome (problems with mozilla)
+                       // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
+                       // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
+                       // debug(xml.childNodes[0].textContent);
+                       var doctext;
+                        if (document.all) { // IE
+                          doctext = xml.childNodes[0].text;
+                        } else {
+                          doctext= xml.childNodes[0].textContent;
+                        }
+                       showDoc(uri,doctext,id,docWin);
+
+               } else {
+                       debug("file open failed");
+               }
+       };
+       callServer("open",processor,"file=" + escape(thefile) + "&readonly=true"); 
+}
+
+function createDocWin(uri) {
+  var title = "Matita Browser - " + uri;
+  var docWin = window.open( "", "matitabrowser",
+     "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
+  docWin.document.write('<html><head><title>' + title + '</title>' +
+                        '<script type="text/javascript" src="jquery.js"></script>' +
+                        '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
+                        '<script type="text/javascript" src="matitaweb.js"></script>' +
+                        '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
+                        '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
+                       '</head>');     
+  docWin.document.write('<body><H1>'+ uri + '</H1>' + 
+                     '<pre id="locked"></pre></body></html>');
+  docWin.document.close();
+  docWin.baseuri = uri;
+  return docWin;
+}
+
+function showDoc(uri,doctext,id,docWin) {
+  var outarea = docWin.document.getElementById("locked");
+  outarea.innerHTML = doctext;
+  try {
+         docWin.document.getElementById(id).scrollIntoView(true);
+  } catch (e) { }
+  docWin.init_hyperlinks();
+  docWin.init_autotraces();
+}
+
 function showLibrary(title,callback,reloadDialog)
 { 
        var req = null;
Unnamed repository; edit this file 'description' to name the repository.