X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=6661cd04ad5959b28ae8f6d8ff49341dc441eeb7;hb=5310bb693a61b4c2c51bbd05e5ef9a4b764012cd;hp=20d0fec43dbcf9557da473af7fae857413b3d60e;hpb=0c442e9d5804a828b4a7ae6eb8a172ded6f477c9;p=helm.git
diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 20d0fec43..6661cd04a 100644
--- 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('Matita Log' + '');
logWin.document.write('');
@@ -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('' + title + '' +
+ '' +
+ '' +
+ '' +
+ '' +
+ '' +
+ '');
+ docWin.document.write(''+ uri + '
' +
+ '');
+ 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;