use_text etc.: proper output of error messages;

--- a/src/Pure/ML-Systems/polyml-4.0.ML	Tue Jan 16 00:35:18 2001 +0100
+++ b/src/Pure/ML-Systems/polyml-4.0.ML	Tue Jan 16 00:35:50 2001 +0100
@@ -68,10 +68,11 @@
 
 in
 
-fun use_text print verbose txt =
+fun use_text (print, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
+    fun output () = drop_last_char (implode (rev (! out_buffer)));
 
     fun get () =
       (case ! in_buffer of
@@ -83,11 +84,9 @@
       (case ! in_buffer of
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
-
-    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
   in
-    exec () handle exn => (show_output (); raise exn);
-    if verbose then show_output () else ()
+    exec () handle exn => (err (output ()); raise exn);
+    if verbose then print (output ()) else ()
   end;
 
 end;

--- a/src/Pure/ML-Systems/polyml.ML	Tue Jan 16 00:35:18 2001 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 16 00:35:50 2001 +0100
@@ -59,10 +59,11 @@
 
 in
 
-fun use_text print verbose txt =
+fun use_text (print, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
+    fun output () = drop_last_char (implode (rev (! out_buffer)));
 
     fun get () =
       (case ! in_buffer of
@@ -74,11 +75,9 @@
       (case ! in_buffer of
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
-
-    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
   in
-    exec () handle exn => (show_output (); raise exn);
-    if verbose then show_output () else ()
+    exec () handle exn => (err (output ()); raise exn);
+    if verbose then print (output ()) else ()
   end;
 
 

--- a/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:18 2001 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:50 2001 +0100
@@ -80,22 +80,21 @@
 
 (* ML command execution *)
 
-fun use_text print verbose txt =
+fun use_text (print, err) verbose txt =
   let
     val ref out_orig = Compiler.Control.Print.out;
 
     val out_buffer = ref ([]: string list);
     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
-
-    fun show_output () =
+    fun output () =
       let val str = implode (rev (! out_buffer))
-      in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
+      in String.substring (str, 0, Int.max (0, size str - 1)) end;
   in
     Compiler.Control.Print.out := out;
     Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
-      (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
+      (Compiler.Control.Print.out := out_orig; err (output ()); raise exn);
     Compiler.Control.Print.out := out_orig;
-    if verbose then show_output () else ()
+    if verbose then print (output ()) else ()
   end;
 
 

--- a/src/Pure/Thy/thm_database.ML	Tue Jan 16 00:35:18 2001 +0100
+++ b/src/Pure/Thy/thm_database.ML	Tue Jan 16 00:35:50 2001 +0100
@@ -68,7 +68,7 @@
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text priority true;
+val use_text_verbose = use_text Context.ml_output true;
 
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in

--- a/src/Pure/context.ML	Tue Jan 16 00:35:18 2001 +0100
+++ b/src/Pure/context.ML	Tue Jan 16 00:35:50 2001 +0100
@@ -22,6 +22,7 @@
   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
   val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
+  val ml_output: (string -> unit) * (string -> unit)
   val use_mltext: string -> bool -> theory option -> unit
   val use_mltext_theory: string -> bool -> theory -> theory
   val use_let: string -> string -> string -> theory -> theory
@@ -69,8 +70,10 @@
 
 (* use ML text *)
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text priority verb txt) ();
-fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text priority verb) txt);
+val ml_output = (writeln, error_msg: string -> unit);
+
+fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text ml_output verb txt) ();
+fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text ml_output verb) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;