# HG changeset patch # User wenzelm # Date 1553982698 -3600 # Node ID a8142ac5e4b6c3cc0e7b26f292f4b4aee9f57aaa # Parent c8e08d8ffb93373bcf24718f03416d8296724457 more PIDE markup and hyperlinks; diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Mar 30 22:51:38 2019 +0100 @@ -65,6 +65,7 @@ val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T + val export_pathN: string val export_path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T val markupN: string @@ -397,6 +398,7 @@ (* external resources *) val (pathN, path) = markup_string "path" nameN; +val (export_pathN, export_path) = markup_string "export_path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Pure/PIDE/markup.scala Sat Mar 30 22:51:38 2019 +0100 @@ -200,6 +200,9 @@ val PATH = "path" val Path = new Markup_String(PATH, NAME) + val EXPORT_PATH = "export_path" + val Export_Path = new Markup_String(EXPORT_PATH, NAME) + val URL = "url" val Url = new Markup_String(URL, NAME) diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Pure/Thy/export.ML Sat Mar 30 22:51:38 2019 +0100 @@ -23,14 +23,23 @@ type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}; -fun export_params ({theory, binding, executable, compress}: params) blob = - (Output.try_protocol_message o Markup.export) - {id = Position.get_id (Position.thread_data ()), - serial = serial (), - theory_name = Context.theory_long_name theory, - name = Path.implode_binding binding, - executable = executable, - compress = compress} blob; +fun export_params ({theory = thy, binding, executable, compress}: params) blob = + let + val theory_name = Context.theory_long_name thy; + val name = Path.implode_binding binding; + val (path, pos) = Path.dest_binding binding; + val _ = + Context_Position.report_generic (Context.Theory thy) pos + (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path))); + in + (Output.try_protocol_message o Markup.export) + {id = Position.get_id (Position.thread_data ()), + serial = serial (), + theory_name = theory_name, + name = name, + executable = executable, + compress = compress} blob + end; fun export thy binding blob = export_params {theory = thy, binding = binding, executable = false, compress = true} blob; diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Tools/jEdit/src/active.scala Sat Mar 30 22:51:38 2019 +0100 @@ -47,7 +47,7 @@ case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) => GUI_Thread.later { val name = Markup.Name.unapply(props) getOrElse "" - VFSBrowser.browseDirectory(view, Isabelle_Export.vfs_prefix + name) + PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view) } case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) => diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 30 22:51:38 2019 +0100 @@ -14,6 +14,7 @@ import org.gjt.sp.jedit.{jEdit, View, Buffer} import org.gjt.sp.jedit.browser.VFSBrowser +import org.gjt.sp.jedit.io.{VFSManager, VFSFile} class JEdit_Editor extends Editor[View] @@ -155,15 +156,23 @@ case _: IllegalArgumentException => } - case None if (new JFile(name)).isDirectory => - VFSBrowser.browseDirectory(view, name) + case None => + val is_file = + try { + val vfs = VFSManager.getVFSForPath(name) + val vfs_file = vfs._getFile((), name, view) + vfs_file != null && vfs_file.getType == VFSFile.FILE + } + catch { case ERROR(_) => false } - case None => - val args = - if (line <= 0) Array(name) - else if (column <= 0) Array(name, "+line:" + (line + 1)) - else Array(name, "+line:" + (line + 1) + "," + (column + 1)) - jEdit.openFiles(view, null, args) + if (is_file) { + val args = + if (line <= 0) Array(name) + else if (column <= 0) Array(name, "+line:" + (line + 1)) + else Array(name, "+line:" + (line + 1) + "," + (column + 1)) + jEdit.openFiles(view, null, args) + } + else VFSBrowser.browseDirectory(view, name) } } diff -r c8e08d8ffb93 -r a8142ac5e4b6 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 30 20:54:47 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 30 22:51:38 2019 +0100 @@ -124,8 +124,8 @@ Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) private val hyperlink_elements = - Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.POSITION, - Markup.CITATION) + Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL, + Markup.POSITION, Markup.CITATION) private val gutter_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) @@ -242,6 +242,10 @@ val link = PIDE.editor.hyperlink_file(true, file) Some(links :+ Text.Info(snapshot.convert(info_range), link)) + case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) => + val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name) + Some(links :+ Text.Info(snapshot.convert(info_range), link)) + case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) => PIDE.editor.hyperlink_doc(name).map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))