--- 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 *)
--- 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 */
--- 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)))
--- 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;
--- 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
--- 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))