+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();
+}
+