# HG changeset patch # User wenzelm # Date 1547470692 -3600 # Node ID c95edf19133b5d3718dd6f619cc7db4b9da2c2fd # Parent e61b0b819d288bb01c7df55fad9935dd715cc6b4 clarified message; diff -r e61b0b819d28 -r c95edf19133b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Jan 14 13:58:12 2019 +0100 @@ -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"; diff -r e61b0b819d28 -r c95edf19133b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Jan 14 13:58:12 2019 +0100 @@ -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" diff -r e61b0b819d28 -r c95edf19133b src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Jan 14 13:58:12 2019 +0100 @@ -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))) diff -r e61b0b819d28 -r c95edf19133b src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Pure/Thy/export.ML Mon Jan 14 13:58:12 2019 +0100 @@ -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; diff -r e61b0b819d28 -r c95edf19133b src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Tools/Code/code_target.ML Mon Jan 14 13:58:12 2019 +0100 @@ -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) diff -r e61b0b819d28 -r c95edf19133b src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Tools/jEdit/src/active.scala Mon Jan 14 13:58:12 2019 +0100 @@ -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)) diff -r e61b0b819d28 -r c95edf19133b src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Jan 14 13:58:12 2019 +0100 @@ -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 diff -r e61b0b819d28 -r c95edf19133b src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 14 13:58:12 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.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))