src/Pure/ML-Systems/smlnj.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5708 fb09ab6a447f
equal deleted inserted replaced
5089:f95e0a6eb775 5090:75ac9b451ae0
    80 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
    80 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
    81 
    81 
    82 
    82 
    83 (* ML command execution *)
    83 (* ML command execution *)
    84 
    84 
    85 val use_text = Compiler.Interact.useStream o TextIO.openString;
    85 fun use_text verbose txt =
       
    86   let
       
    87     val ref out_orig = Compiler.Control.Print.out;
       
    88 
       
    89     val out_buffer = ref ([]: string list);
       
    90     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
       
    91 
       
    92     fun show_output () = print (implode (rev (! out_buffer)));
       
    93   in
       
    94     Compiler.Control.Print.out := out;
       
    95     Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
       
    96       (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
       
    97     Compiler.Control.Print.out := out_orig;
       
    98     if verbose then show_output () else ()
       
    99   end;
    86 
   100 
    87 
   101 
    88 
   102 
    89 (** OS related **)
   103 (** OS related **)
    90 
   104