--- 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;