1.1 --- a/src/Pure/ML-Systems/mlworks.ML	Fri Jun 26 15:16:14 1998 +0200
     1.2 +++ b/src/Pure/ML-Systems/mlworks.ML	Mon Jun 29 10:32:06 1998 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  (* ML command execution *)
     1.5  
     1.6  (*Can one redirect 'use' directly to an instream?*)
     1.7 -fun use_text txt =
     1.8 +fun use_text _ txt =
     1.9    let
    1.10      val tmp_name = OS.FileSys.tmpName ();
    1.11      val tmp_file = TextIO.openOut tmp_name;

     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Fri Jun 26 15:16:14 1998 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Jun 29 10:32:06 1998 +0200
     2.3 @@ -41,18 +41,27 @@
     2.4  
     2.5  (* ML command execution -- 'eval' *)
     2.6  
     2.7 -fun use_text txt =
     2.8 +fun use_text verbose txt =
     2.9    let
    2.10 -    val buffer = ref (explode txt);
    2.11 +    val in_buffer = ref (explode txt);
    2.12 +    val out_buffer = ref ([]: string list);
    2.13 +
    2.14      fun get () =
    2.15 -      (case ! buffer of
    2.16 +      (case ! in_buffer of
    2.17          [] => ""
    2.18 -      | c :: cs => (buffer := cs; c));
    2.19 +      | c :: cs => (in_buffer := cs; c));
    2.20 +    fun put s = out_buffer := s :: ! out_buffer;
    2.21 +
    2.22      fun exec () =
    2.23 -      (case ! buffer of
    2.24 +      (case ! in_buffer of
    2.25          [] => ()
    2.26 -      | _ => (PolyML.compiler (get, print) (); exec ()));
    2.27 -  in exec () end;
    2.28 +      | _ => (PolyML.compiler (get, put) (); exec ()));
    2.29 +
    2.30 +    fun show_output () = print (implode (rev (! out_buffer)));
    2.31 +  in
    2.32 +    exec () handle exn => (show_output (); raise exn);
    2.33 +    if verbose then show_output () else ()
    2.34 +  end;
    2.35  
    2.36  
    2.37  

     3.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Jun 26 15:16:14 1998 +0200
     3.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 29 10:32:06 1998 +0200
     3.3 @@ -81,7 +81,7 @@
     3.4  
     3.5  (* ML command execution *)
     3.6  
     3.7 -val use_text = System.Compile.use_stream o open_string;
     3.8 +fun use_text _ = System.Compile.use_stream o open_string;
     3.9  
    3.10  
    3.11  

     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Jun 26 15:16:14 1998 +0200
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jun 29 10:32:06 1998 +0200
     4.3 @@ -82,7 +82,21 @@
     4.4  
     4.5  (* ML command execution *)
     4.6  
     4.7 -val use_text = Compiler.Interact.useStream o TextIO.openString;
     4.8 +fun use_text verbose txt =
     4.9 +  let
    4.10 +    val ref out_orig = Compiler.Control.Print.out;
    4.11 +
    4.12 +    val out_buffer = ref ([]: string list);
    4.13 +    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
    4.14 +
    4.15 +    fun show_output () = print (implode (rev (! out_buffer)));
    4.16 +  in
    4.17 +    Compiler.Control.Print.out := out;
    4.18 +    Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
    4.19 +      (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
    4.20 +    Compiler.Control.Print.out := out_orig;
    4.21 +    if verbose then show_output () else ()
    4.22 +  end;
    4.23  
    4.24  
    4.25  

     5.1 --- a/src/Pure/Thy/thm_database.ML	Fri Jun 26 15:16:14 1998 +0200
     5.2 +++ b/src/Pure/Thy/thm_database.ML	Mon Jun 29 10:32:06 1998 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4    let val thm' = store_thm (name, thm) in
     5.5      if is_ml_identifier name then
     5.6        (qed_thm := Some thm';
     5.7 -        use_text ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
     5.8 +        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
     5.9      else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
    5.10    end;
    5.11  

     6.1 --- a/src/Pure/Thy/thy_read.ML	Fri Jun 26 15:16:14 1998 +0200
     6.2 +++ b/src/Pure/Thy/thy_read.ML	Mon Jun 29 10:32:06 1998 +0200
     6.3 @@ -267,7 +267,7 @@
     6.4               Use.use ml_file);
     6.5  
     6.6         (*Store theory again because it could have been redefined*)
     6.7 -       use_text ("val _ = store_theory " ^ tname ^ ".thy;");
     6.8 +       use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
     6.9  
    6.10         (*Add theory to list of all loaded theories (for index.html)
    6.11           and add it to its parents' sub-charts*)