// 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;
in
match ast with
+ | GrafiteAst.Executable (_,
+ GrafiteAst.NCommand (_,
+ GrafiteAst.NObj (loc, astobj,_))) ->
+ let objname = NotationPt.name_of_obj astobj in
+ let status =
+ MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
+ in
+ let new_parsed_text = Ulexing.from_utf8_string parsed_text in
+ let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
+ let outstr = ref "" in
+ ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text);
+ let x, y = HExtlib.loc_of_floc floc in
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x !outstr in
+ let post = Netconversion.ustring_sub `Enc_utf8 x
+ (Netconversion.ustring_length `Enc_utf8 !outstr - x) !outstr in
+ outstr := Printf.sprintf
+ "%s\005input type=\"radio\" class=\"anchor\" id=\"%s\" /\006%s" pre objname post;
+ prerr_endline ("baseuri after advance = " ^ status#baseuri);
+ (* prerr_endline ("parser output: " ^ !outstr); *)
+ (status,!outstr, unparsed_txt'),parsed_text_len
| GrafiteAst.Executable (_,
GrafiteAst.NTactic (_,
[GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params
~content_type:"text/xml; charset=\"utf-8\""
();
*)
+ let readonly = cgi # argument_value "readonly" in
let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
(* prerr_endline ("reading file " ^ filename); *)
let body =
with
Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
include_paths := incpaths;
- let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
- let history = [status] in
- MatitaAuthentication.set_status sid status;
- MatitaAuthentication.set_history sid history;
+ if readonly <> "true" then
+ (let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
+ let history = [status] in
+ MatitaAuthentication.set_status sid status;
+ MatitaAuthentication.set_history sid history);
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
projects / helm.git / commitdiff