From: Wilmer Ricciotti Date: Thu, 21 Jun 2012 11:41:16 +0000 (+0000) Subject: Hyperlink support. X-Git-Tag: make_still_working~1631 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5310bb693a61b4c2c51bbd05e5ef9a4b764012cd Hyperlink support. --- 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; diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 1e5a0c700..fd7696173 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -213,6 +213,26 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script 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 @@ -362,6 +382,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~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 = @@ -386,10 +407,11 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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\""