src/Pure/Thy/export.ML

 
 signature EXPORT =
 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 _ =
       (case space_explode "/" name of

     compress = compress} body;
 
 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;