src/Pure/ML-Systems/smlnj.ML
changeset 7855 092a6435afad
parent 6227 3198f547f8af
child 7890 0aa16bc2abdb
equal deleted inserted replaced
7854:fe7b7e3c3ddc 7855:092a6435afad
    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 verbose txt =
    83 fun use_text print 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 () => ())};
   187     TextIO.closeIn is;
   187     TextIO.closeIn is;
   188     OS.FileSys.remove tmp_name;
   188     OS.FileSys.remove tmp_name;
   189     result
   189     result
   190   end;
   190   end;
   191 
   191 
       
   192 (*plain version; with return code*)
       
   193 val system = OS.Process.system: string -> int; 
       
   194 
   192 
   195 
   193 (* file handling *)
   196 (* file handling *)
   194 
   197 
   195 (*get time of last modification*)
   198 (*get time of last modification*)
   196 fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
   199 fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";