# HG changeset patch # User wenzelm # Date 1547404926 -3600 # Node ID 97ddaec3e2ae692b997ae2c1b3e721ce227038a6 # Parent cf50cee2adee95f92b7e546fb155ca97426930ed support hyperlink to theory exports; diff -r cf50cee2adee -r 97ddaec3e2ae src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Pure/PIDE/markup.ML Sun Jan 13 19:42:06 2019 +0100 @@ -60,6 +60,7 @@ val pathN: string val path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T + val theory_exportsN: string val theory_exports: string -> T val markupN: string val consistentN: string val unbreakableN: string @@ -373,6 +374,7 @@ val (pathN, path) = markup_string "path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; +val (theory_exportsN, theory_exports) = markup_string "theory_exports" nameN; (* pretty printing *) diff -r cf50cee2adee -r 97ddaec3e2ae src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Pure/PIDE/markup.scala Sun Jan 13 19:42:06 2019 +0100 @@ -196,6 +196,9 @@ val DOC = "doc" val Doc = new Markup_String(DOC, NAME) + val THEORY_EXPORTS = "theory_exports" + val Theory_Exports = new Markup_String(THEORY_EXPORTS, NAME) + /* pretty printing */ diff -r cf50cee2adee -r 97ddaec3e2ae src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Pure/PIDE/rendering.scala Sun Jan 13 19:42:06 2019 +0100 @@ -196,8 +196,8 @@ val tooltip_elements = Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, - Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, - Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ + Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS, + Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) val tooltip_message_elements = @@ -596,6 +596,9 @@ case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => Some(info + (r0, true, XML.Text("URL " + quote(name)))) + case (info, Text.Info(r0, XML.Elem(Markup.Theory_Exports(name), _))) => + Some(info + (r0, true, XML.Text("theory exports " + quote(name)))) + case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body))) diff -r cf50cee2adee -r 97ddaec3e2ae src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Pure/Thy/export.ML Sun Jan 13 19:42:06 2019 +0100 @@ -8,11 +8,15 @@ sig val export: theory -> string -> string list -> unit val export_raw: theory -> string -> string list -> unit + val markup_text: theory -> string -> Markup.T * string + val information: theory -> string -> unit end; structure Export: EXPORT = struct +(* export *) + fun check_name name = let val _ = @@ -32,4 +36,14 @@ val export = gen_export true; val export_raw = gen_export false; + +(* information message *) + +fun markup_text thy s = + (Markup.theory_exports (Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s)), + "theory exports"); + +fun information thy s = + Output.information ("See " ^ uncurry Markup.markup (markup_text thy s)); + end; diff -r cf50cee2adee -r 97ddaec3e2ae src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 13 19:42:06 2019 +0100 @@ -198,6 +198,12 @@ override def toString: String = "doc " + quote(name) }) + def hyperlink_theory_exports(name: String): Hyperlink = + new Hyperlink { + def follow(view: View): Unit = + VFSBrowser.browseDirectory(view, Isabelle_Export.vfs_prefix + name) + } + def hyperlink_url(name: String): Hyperlink = new Hyperlink { override val external = true diff -r cf50cee2adee -r 97ddaec3e2ae src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 13 19:03:16 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 13 19:42:06 2019 +0100 @@ -118,14 +118,14 @@ private val highlight_elements = Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, - Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, - Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, - Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, + Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS, + Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, + Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) private val hyperlink_elements = - Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION, - Markup.CITATION, Markup.URL) + Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS, + Markup.POSITION, Markup.CITATION) private val gutter_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) @@ -250,6 +250,10 @@ val link = PIDE.editor.hyperlink_url(name) Some(links :+ Text.Info(snapshot.convert(info_range), link)) + case (links, Text.Info(info_range, XML.Elem(Markup.Theory_Exports(name), _))) => + val link = PIDE.editor.hyperlink_theory_exports(name) + Some(links :+ Text.Info(snapshot.convert(info_range), link)) + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))