src/Pure/ML-Systems/smlnj-0.93.ML
changeset 7855 092a6435afad
parent 7149 d0c2168f7704
child 12108 b6f10dcde803
equal deleted inserted replaced
7854:fe7b7e3c3ddc 7855:092a6435afad
    88 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    88 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    89 
    89 
    90 
    90 
    91 (* ML command execution *)
    91 (* ML command execution *)
    92 
    92 
    93 fun use_text _ = System.Compile.use_stream o open_string;
    93 fun use_text _ _ = System.Compile.use_stream o open_string;
    94 
    94 
    95 
    95 
    96 
    96 
    97 (** interrupts **)
    97 (** interrupts **)
    98 
    98 
   178     close_in is;
   178     close_in is;
   179     System.Unsafe.SysIO.unlink tmp_name;
   179     System.Unsafe.SysIO.unlink tmp_name;
   180     result
   180     result
   181   end;
   181   end;
   182 
   182 
       
   183 (*plain version; with return code*)
       
   184 fun system cmd = System.system cmd div 256;
       
   185 
   183 
   186 
   184 (* file handling *)
   187 (* file handling *)
   185 
   188 
   186 (*get time of last modification*)
   189 (*get time of last modification*)
   187 local
   190 local