equal
deleted
inserted
replaced
7 use "ML-Systems/exn.ML"; |
7 use "ML-Systems/exn.ML"; |
8 if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then () |
8 if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then () |
9 else use "ML-Systems/universal.ML"; |
9 else use "ML-Systems/universal.ML"; |
10 use "ML-Systems/multithreading.ML"; |
10 use "ML-Systems/multithreading.ML"; |
11 use "ML-Systems/time_limit.ML"; |
11 use "ML-Systems/time_limit.ML"; |
|
12 use "ML-Systems/system_shell.ML"; |
|
13 |
12 |
14 |
13 |
15 |
14 (** ML system and platform related **) |
16 (** ML system and platform related **) |
15 |
17 |
16 (* Compiler options *) |
18 (* Compiler options *) |
188 |
190 |
189 val cd = OS.FileSys.chDir; |
191 val cd = OS.FileSys.chDir; |
190 val pwd = OS.FileSys.getDir; |
192 val pwd = OS.FileSys.getDir; |
191 |
193 |
192 |
194 |
193 (* system command execution *) |
|
194 |
|
195 (*execute Unix command which doesn't take any input from stdin and |
|
196 sends its output to stdout; could be done more easily by Unix.execute, |
|
197 but that function doesn't use the PATH*) |
|
198 fun execute command = |
|
199 let |
|
200 val tmp_name = OS.FileSys.tmpName (); |
|
201 val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); |
|
202 val result = TextIO.inputAll is; |
|
203 in |
|
204 TextIO.closeIn is; |
|
205 OS.FileSys.remove tmp_name; |
|
206 result |
|
207 end; |
|
208 |
|
209 (*plain version; with return code*) |
|
210 fun system cmd = |
|
211 if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1; |
|
212 |
|
213 |
|
214 (*Convert a process ID to a decimal string (chiefly for tracing)*) |
195 (*Convert a process ID to a decimal string (chiefly for tracing)*) |
215 fun string_of_pid pid = |
196 fun string_of_pid pid = |
216 Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid)); |
197 Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid)); |
217 |
198 |
218 |
199 |