src/Pure/ML-Systems/smlnj.ML
changeset 10914 aded4ba99b88
parent 10725 ea048ad15283
child 12108 b6f10dcde803
equal deleted inserted replaced
10913:57eb8c1d6f88 10914:aded4ba99b88
    78 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
    78 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
    79 
    79 
    80 
    80 
    81 (* ML command execution *)
    81 (* ML command execution *)
    82 
    82 
    83 fun use_text print verbose txt =
    83 fun use_text (print, err) verbose txt =
    84   let
    84   let
    85     val ref out_orig = Compiler.Control.Print.out;
    85     val ref out_orig = Compiler.Control.Print.out;
    86 
    86 
    87     val out_buffer = ref ([]: string list);
    87     val out_buffer = ref ([]: string list);
    88     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
    88     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
    89 
    89     fun output () =
    90     fun show_output () =
       
    91       let val str = implode (rev (! out_buffer))
    90       let val str = implode (rev (! out_buffer))
    92       in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
    91       in String.substring (str, 0, Int.max (0, size str - 1)) end;
    93   in
    92   in
    94     Compiler.Control.Print.out := out;
    93     Compiler.Control.Print.out := out;
    95     Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
    94     Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
    96       (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
    95       (Compiler.Control.Print.out := out_orig; err (output ()); raise exn);
    97     Compiler.Control.Print.out := out_orig;
    96     Compiler.Control.Print.out := out_orig;
    98     if verbose then show_output () else ()
    97     if verbose then print (output ()) else ()
    99   end;
    98   end;
   100 
    99 
   101 
   100 
   102 
   101 
   103 (** interrupts **)
   102 (** interrupts **)