src/Pure/ML-Systems/mosml.ML
changeset 26220 d34b68c21f9a
parent 26084 a7475459c740
child 26223 f4a1a96cc07c
equal deleted inserted replaced
26219:2d026932f710 26220:d34b68c21f9a
    36 
    36 
    37 use "ML-Systems/exn.ML";
    37 use "ML-Systems/exn.ML";
    38 use "ML-Systems/universal.ML";
    38 use "ML-Systems/universal.ML";
    39 use "ML-Systems/multithreading.ML";
    39 use "ML-Systems/multithreading.ML";
    40 use "ML-Systems/time_limit.ML";
    40 use "ML-Systems/time_limit.ML";
       
    41 use "ML-Systems/system_shell.ML";
    41 
    42 
    42 
    43 
    43 (*low-level pointer equality*)
    44 (*low-level pointer equality*)
    44 local val cast : 'a -> int = Obj.magic
    45 local val cast : 'a -> int = Obj.magic
    45 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
    46 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
   176 
   177 
   177 
   178 
   178 
   179 
   179 (** OS related **)
   180 (** OS related **)
   180 
   181 
   181 (* current directory *)
       
   182 
       
   183 val cd = OS.FileSys.chDir;
   182 val cd = OS.FileSys.chDir;
   184 val pwd = OS.FileSys.getDir;
   183 val pwd = OS.FileSys.getDir;
   185 
   184 
   186 
       
   187 (* system command execution *)
       
   188 
       
   189 (*execute Unix command which doesn't take any input from stdin and
       
   190   sends its output to stdout; could be done more easily by Unix.execute,
       
   191   but that function doesn't use the PATH*)
       
   192 fun execute command =
       
   193   let
       
   194     val tmp_name = FileSys.tmpName ();
       
   195     val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
       
   196     val result = TextIO.inputAll is;
       
   197   in
       
   198     TextIO.closeIn is;
       
   199     FileSys.remove tmp_name;
       
   200     result
       
   201   end;
       
   202 
       
   203 (*plain version; with return code*)
       
   204 fun system cmd =
       
   205   if Process.system cmd = Process.success then 0 else 1;
       
   206 
       
   207 
       
   208 val string_of_pid = Int.toString;
   185 val string_of_pid = Int.toString;
   209 
       
   210 
       
   211 (* getenv *)
       
   212 
   186 
   213 fun getenv var =
   187 fun getenv var =
   214   (case Process.getEnv var of
   188   (case Process.getEnv var of
   215     NONE => ""
   189     NONE => ""
   216   | SOME txt => txt);
   190   | SOME txt => txt);