// 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,
function changeFile(name) {
current_fname = name;
matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+ baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
}
function init_keyboard(target)
}
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)
}
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>');
if (is_defined(xml)) {
advOneStep(xml);
populate_goalarray(metasenv);
+ init_hyperlinks();
init_autotraces();
} else {
debug("advance failed");
}
unlocked.scrollIntoView(true);
metasenv = xml.getElementsByTagName("meta");
+ init_hyperlinks();
init_autotraces();
populate_goalarray(metasenv);
unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
lockedbackup = "";
locked.innerHTML = lockedbackup;
+ init_hyperlinks();
init_autotraces();
hideSequent();
+ strip_anchors();
unlocked.scrollIntoView(true);
} else {
debug("goto top failed");
*/
var len = advOneStep(xml);
if (offset <= len) {
+ init_hyperlinks();
init_autotraces();
populate_goalarray(metasenv);
resume();
gotoPos(offset - len);
}
} catch (er) {
+ init_hyperlinks();
init_autotraces();
populate_goalarray(metasenv);
resume();
}
} else {
+ init_hyperlinks();
init_autotraces();
unlocked.scrollIntoView(true);
populate_goalarray(metasenv);
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");
lockedbackup = "";
locked.innerHTML = lockedbackup;
unlocked.innerHTML = xml.documentElement.wholeText;
+ strip_anchors();
} else {
debug("file open failed");
}
} else {
unlocked.innerHTML = xml.childNodes[0].textContent;
}
+ strip_anchors();
+ init_hyperlinks();
init_autotraces();
} else {
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;