use_text etc.: proper output of error messages;
authorwenzelm
Tue Jan 16 00:35:50 2001 +0100 (2001-01-16)
changeset 10914aded4ba99b88
parent 10913 57eb8c1d6f88
child 10915 6b66a8a530ce
use_text etc.: proper output of error messages;
src/Pure/ML-Systems/polyml-4.0.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/Thy/thm_database.ML
src/Pure/context.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-4.0.ML	Tue Jan 16 00:35:18 2001 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-4.0.ML	Tue Jan 16 00:35:50 2001 +0100
     1.3 @@ -68,10 +68,11 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun use_text print verbose txt =
     1.8 +fun use_text (print, err) verbose txt =
     1.9    let
    1.10      val in_buffer = ref (explode txt);
    1.11      val out_buffer = ref ([]: string list);
    1.12 +    fun output () = drop_last_char (implode (rev (! out_buffer)));
    1.13  
    1.14      fun get () =
    1.15        (case ! in_buffer of
    1.16 @@ -83,11 +84,9 @@
    1.17        (case ! in_buffer of
    1.18          [] => ()
    1.19        | _ => (PolyML.compiler (get, put) (); exec ()));
    1.20 -
    1.21 -    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
    1.22    in
    1.23 -    exec () handle exn => (show_output (); raise exn);
    1.24 -    if verbose then show_output () else ()
    1.25 +    exec () handle exn => (err (output ()); raise exn);
    1.26 +    if verbose then print (output ()) else ()
    1.27    end;
    1.28  
    1.29  end;
     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Jan 16 00:35:18 2001 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 16 00:35:50 2001 +0100
     2.3 @@ -59,10 +59,11 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun use_text print verbose txt =
     2.8 +fun use_text (print, err) verbose txt =
     2.9    let
    2.10      val in_buffer = ref (explode txt);
    2.11      val out_buffer = ref ([]: string list);
    2.12 +    fun output () = drop_last_char (implode (rev (! out_buffer)));
    2.13  
    2.14      fun get () =
    2.15        (case ! in_buffer of
    2.16 @@ -74,11 +75,9 @@
    2.17        (case ! in_buffer of
    2.18          [] => ()
    2.19        | _ => (PolyML.compiler (get, put) (); exec ()));
    2.20 -
    2.21 -    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
    2.22    in
    2.23 -    exec () handle exn => (show_output (); raise exn);
    2.24 -    if verbose then show_output () else ()
    2.25 +    exec () handle exn => (err (output ()); raise exn);
    2.26 +    if verbose then print (output ()) else ()
    2.27    end;
    2.28  
    2.29  
     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:18 2001 +0100
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:50 2001 +0100
     3.3 @@ -80,22 +80,21 @@
     3.4  
     3.5  (* ML command execution *)
     3.6  
     3.7 -fun use_text print verbose txt =
     3.8 +fun use_text (print, err) verbose txt =
     3.9    let
    3.10      val ref out_orig = Compiler.Control.Print.out;
    3.11  
    3.12      val out_buffer = ref ([]: string list);
    3.13      val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
    3.14 -
    3.15 -    fun show_output () =
    3.16 +    fun output () =
    3.17        let val str = implode (rev (! out_buffer))
    3.18 -      in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
    3.19 +      in String.substring (str, 0, Int.max (0, size str - 1)) end;
    3.20    in
    3.21      Compiler.Control.Print.out := out;
    3.22      Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
    3.23 -      (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
    3.24 +      (Compiler.Control.Print.out := out_orig; err (output ()); raise exn);
    3.25      Compiler.Control.Print.out := out_orig;
    3.26 -    if verbose then show_output () else ()
    3.27 +    if verbose then print (output ()) else ()
    3.28    end;
    3.29  
    3.30  
     4.1 --- a/src/Pure/Thy/thm_database.ML	Tue Jan 16 00:35:18 2001 +0100
     4.2 +++ b/src/Pure/Thy/thm_database.ML	Tue Jan 16 00:35:50 2001 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4    else if name = "" then true
     4.5    else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
     4.6  
     4.7 -val use_text_verbose = use_text priority true;
     4.8 +val use_text_verbose = use_text Context.ml_output true;
     4.9  
    4.10  fun ml_store_thm (name, thm) =
    4.11    let val thm' = store_thm (name, thm) in
     5.1 --- a/src/Pure/context.ML	Tue Jan 16 00:35:18 2001 +0100
     5.2 +++ b/src/Pure/context.ML	Tue Jan 16 00:35:50 2001 +0100
     5.3 @@ -22,6 +22,7 @@
     5.4    val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
     5.5    val save: ('a -> 'b) -> 'a -> 'b
     5.6    val >> : (theory -> theory) -> unit
     5.7 +  val ml_output: (string -> unit) * (string -> unit)
     5.8    val use_mltext: string -> bool -> theory option -> unit
     5.9    val use_mltext_theory: string -> bool -> theory -> theory
    5.10    val use_let: string -> string -> string -> theory -> theory
    5.11 @@ -69,8 +70,10 @@
    5.12  
    5.13  (* use ML text *)
    5.14  
    5.15 -fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text priority verb txt) ();
    5.16 -fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text priority verb) txt);
    5.17 +val ml_output = (writeln, error_msg: string -> unit);
    5.18 +
    5.19 +fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text ml_output verb txt) ();
    5.20 +fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text ml_output verb) txt);
    5.21  
    5.22  fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    5.23