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;