--- a/src/Pure/PIDE/markup.ML Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Pure/PIDE/markup.ML Mon Jan 14 14:19:00 2019 +0000
@@ -60,7 +60,6 @@
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
@@ -193,6 +192,7 @@
val intensifyN: string val intensify: T
val browserN: string
val graphviewN: string
+ val theory_exportsN: string
val sendbackN: string
val paddingN: string
val padding_line: Properties.entry
@@ -374,7 +374,6 @@
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 *)
@@ -631,6 +630,7 @@
val browserN = "browser"
val graphviewN = "graphview";
+val theory_exportsN = "theory_exports";
val sendbackN = "sendback";
val paddingN = "padding";
--- a/src/Pure/PIDE/markup.scala Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Pure/PIDE/markup.scala Mon Jan 14 14:19:00 2019 +0000
@@ -196,9 +196,6 @@
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 */
@@ -506,6 +503,7 @@
val BROWSER = "browser"
val GRAPHVIEW = "graphview"
+ val THEORY_EXPORTS = "theory_exports"
val SENDBACK = "sendback"
val PADDING = "padding"
--- a/src/Pure/PIDE/rendering.scala Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Pure/PIDE/rendering.scala Mon Jan 14 14:19:00 2019 +0000
@@ -178,7 +178,7 @@
val citation_elements = Markup.Elements(Markup.CITATION)
val active_elements =
- Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+ Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS,
Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
val background_elements =
@@ -196,7 +196,7 @@
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.THEORY_EXPORTS,
+ Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL,
Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
Markup.Elements(tooltip_descriptions.keySet)
@@ -596,9 +596,6 @@
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 Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Pure/Thy/export.ML Mon Jan 14 14:19:00 2019 +0000
@@ -8,8 +8,8 @@
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
+ val markup: theory -> string -> Markup.T
+ val message: theory -> string -> string
end;
structure Export: EXPORT =
@@ -39,11 +39,11 @@
(* information message *)
-fun markup_text thy s =
- (Markup.theory_exports (Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s)),
- "theory exports");
+fun markup thy s =
+ let val name = (Markup.nameN, Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s))
+ in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
-fun information thy s =
- Output.information ("See " ^ uncurry Markup.markup (markup_text thy s));
+fun message thy s =
+ "See " ^ Markup.markup (markup thy s) "theory exports";
end;
--- a/src/Tools/Code/code_target.ML Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Tools/Code/code_target.ML Mon Jan 14 14:19:00 2019 +0000
@@ -177,7 +177,7 @@
());
fun export_information thy name content =
- (Export.export thy name [content]; Export.information thy "");
+ (Export.export thy name [content]; writeln (Export.message thy ""));
fun export_to_exports thy width (Singleton (extension, p)) =
export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)
--- a/src/Tools/jEdit/src/active.scala Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Tools/jEdit/src/active.scala Mon Jan 14 14:19:00 2019 +0000
@@ -10,6 +10,7 @@
import isabelle._
import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.browser.VFSBrowser
object Active
@@ -43,6 +44,12 @@
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
+ 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)
+ }
+
case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
GUI_Thread.later {
view.getInputHandler.invokeAction(XML.content(body))
--- a/src/Tools/jEdit/src/jEdit.props Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Tools/jEdit/src/jEdit.props Mon Jan 14 14:19:00 2019 +0000
@@ -298,6 +298,8 @@
vfs.favorite.2=$JEDIT_HOME
vfs.favorite.3.type=1
vfs.favorite.3=$JEDIT_SETTINGS
+vfs.favorite.4.type=1
+vfs.favorite.4=isabelle-export:
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Jan 14 14:19:00 2019 +0000
@@ -198,12 +198,6 @@
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 Mon Jan 14 11:59:19 2019 +0000
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 14 14:19:00 2019 +0000
@@ -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.THEORY_EXPORTS,
+ 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.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
private val hyperlink_elements =
- Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS,
- Markup.POSITION, Markup.CITATION)
+ Markup.Elements(Markup.ENTITY, Markup.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)
@@ -250,10 +250,6 @@
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))