src/Pure/General/secure.ML

--- a/src/Pure/General/secure.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/General/secure.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -14,6 +14,7 @@
   val use_file: ML_NameSpace.nameSpace ->
     (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
+  val toplevel_pp: string list -> string -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
   val system: string -> int
@@ -41,6 +42,8 @@
 
 fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
 fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
+fun raw_toplevel_pp x =
+  toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
 
 fun use_text ns pos pr verbose txt =
   (secure_mltext (); raw_use_text ns pos pr verbose txt);
@@ -50,6 +53,8 @@
 
 fun use name = use_file ML_NameSpace.global Output.ml_output true name;
 
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+
 (*commit is dynamically bound!*)
 fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
 
@@ -73,5 +78,6 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;