| author | haftmann | 
| Tue, 28 Jun 2005 11:59:38 +0200 | |
| changeset 16577 | 19eff9bc7eee | 
| parent 16516 | 0842635545c3 | 
| child 16659 | 1cf39eba29fe | 
| permissions | -rw-r--r-- | 
| 2341 | 1 | (* Title: Pure/ML-Systems/polyml.ML | 
| 2 | ID: $Id$ | |
| 3 | Author: Lawrence C Paulson, Cambridge University Computer Laboratory | |
| 4 | Copyright 1991 University of Cambridge | |
| 5 | ||
| 14870 | 6 | Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x). | 
| 2341 | 7 | *) | 
| 8 | ||
| 16374 | 9 | (** ML system and platform related **) | 
| 10 | ||
| 16453 
af3afdbd09ea
PolyML.Compiler.printInAlphabeticalOrder := false;
 wenzelm parents: 
16374diff
changeset | 11 | PolyML.Compiler.printInAlphabeticalOrder := false; | 
| 
af3afdbd09ea
PolyML.Compiler.printInAlphabeticalOrder := false;
 wenzelm parents: 
16374diff
changeset | 12 | |
| 
af3afdbd09ea
PolyML.Compiler.printInAlphabeticalOrder := false;
 wenzelm parents: 
16374diff
changeset | 13 | |
| 16374 | 14 | (* cygwin *) | 
| 15 | ||
| 16 | val cygwin_platform = | |
| 17 | let val n = size ml_platform | |
| 18 | in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end; | |
| 19 | ||
| 20 | fun if_cygwin f x = if cygwin_platform then f x else (); | |
| 21 | fun unless_cygwin f x = if not cygwin_platform then f x else (); | |
| 22 | ||
| 2341 | 23 | |
| 16516 | 24 | (*low-level pointer equality*) | 
| 25 | val pointer_eq = Address.wordEq; | |
| 16502 | 26 | |
| 27 | ||
| 11078 | 28 | (* old Poly/ML emulation *) | 
| 2341 | 29 | |
| 11078 | 30 | local | 
| 31 | val orig_exit = exit; | |
| 32 | in | |
| 33 | open PolyML; | |
| 34 | val exit = orig_exit; | |
| 35 | fun quit () = exit 0; | |
| 7148 | 36 | end; | 
| 6042 | 37 | |
| 2341 | 38 | |
| 11078 | 39 | (* restore old-style character / string functions *) | 
| 3588 | 40 | |
| 11078 | 41 | val ord = SML90.ord; | 
| 42 | val chr = SML90.chr; | |
| 43 | val explode = SML90.explode; | |
| 44 | val implode = SML90.implode; | |
| 45 | ||
| 14870 | 46 | |
| 14519 
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
 skalberg parents: 
12989diff
changeset | 47 | (* compiler-independent timing functions *) | 
| 2341 | 48 | |
| 14519 
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
 skalberg parents: 
12989diff
changeset | 49 | use "ML-Systems/cpu-timer-basis.ML"; | 
| 2341 | 50 | |
| 14870 | 51 | |
| 14850 | 52 | (* bounded time execution *) | 
| 53 | ||
| 16374 | 54 | unless_cygwin | 
| 55 | use "ML-Systems/polyml-time-limit.ML"; | |
| 14850 | 56 | |
| 14870 | 57 | |
| 4977 | 58 | (* prompts *) | 
| 59 | ||
| 4984 | 60 | fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); | 
| 4977 | 61 | |
| 62 | ||
| 3588 | 63 | (* toplevel pretty printing (see also Pure/install_pp.ML) *) | 
| 2341 | 64 | |
| 11078 | 65 | fun make_pp _ pprint (str, blk, brk, en) _ _ obj = | 
| 2341 | 66 | pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), | 
| 67 | fn () => brk (99999, 0), en); | |
| 68 | ||
| 69 | ||
| 3588 | 70 | (* ML command execution -- 'eval' *) | 
| 71 | ||
| 7890 | 72 | local | 
| 73 | ||
| 74 | fun drop_last [] = [] | |
| 75 | | drop_last [x] = [] | |
| 76 | | drop_last (x :: xs) = x :: drop_last xs; | |
| 77 | ||
| 78 | in | |
| 79 | ||
| 10914 | 80 | fun use_text (print, err) verbose txt = | 
| 3588 | 81 | let | 
| 5090 | 82 | val in_buffer = ref (explode txt); | 
| 83 | val out_buffer = ref ([]: string list); | |
| 15832 | 84 | fun output () = implode (drop_last (rev (! out_buffer))); | 
| 5090 | 85 | |
| 5038 | 86 | fun get () = | 
| 5090 | 87 | (case ! in_buffer of | 
| 5038 | 88 | [] => "" | 
| 5090 | 89 | | c :: cs => (in_buffer := cs; c)); | 
| 90 | fun put s = out_buffer := s :: ! out_buffer; | |
| 91 | ||
| 5038 | 92 | fun exec () = | 
| 5090 | 93 | (case ! in_buffer of | 
| 5038 | 94 | [] => () | 
| 5090 | 95 | | _ => (PolyML.compiler (get, put) (); exec ())); | 
| 96 | in | |
| 10914 | 97 | exec () handle exn => (err (output ()); raise exn); | 
| 98 | if verbose then print (output ()) else () | |
| 5090 | 99 | end; | 
| 3588 | 100 | |
| 11078 | 101 | end; | 
| 102 | ||
| 103 | ||
| 15832 | 104 | (*eval command line arguments*) | 
| 105 | local | |
| 106 | fun println s = | |
| 107 | (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut); | |
| 15851 | 108 | val eval = use_text (println, println) true; | 
| 15832 | 109 | in | 
| 110 | val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ())); | |
| 111 | end; | |
| 112 | ||
| 113 | ||
| 11078 | 114 | |
| 115 | (** interrupts **) | |
| 116 | ||
| 117 | exception Interrupt = SML90.Interrupt; | |
| 118 | ||
| 119 | local | |
| 120 | ||
| 12989 | 121 | fun capture f x = ((f x): unit; NONE) handle exn => SOME exn; | 
| 11078 | 122 | |
| 12989 | 123 | fun release NONE = () | 
| 124 | | release (SOME exn) = raise exn; | |
| 3588 | 125 | |
| 11078 | 126 | val sig_int = 2; | 
| 127 | ||
| 128 | fun change_signal new_handler f x = | |
| 129 | let | |
| 130 | (*RACE wrt. other signals*) | |
| 131 | val old_handler = Signal.signal (sig_int, new_handler); | |
| 132 | val result = capture f x; | |
| 133 | val _ = Signal.signal (sig_int, old_handler); | |
| 134 | in release result end; | |
| 5813 | 135 | |
| 11078 | 136 | val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()); | 
| 137 | ||
| 138 | in | |
| 139 | ||
| 140 | val _ = Signal.signal (sig_int, default_handler); | |
| 141 | ||
| 12989 | 142 | fun ignore_interrupt f = change_signal Signal.SIG_IGN f; | 
| 143 | fun raise_interrupt f = change_signal default_handler f; | |
| 11078 | 144 | |
| 145 | end; | |
| 5813 | 146 | |
| 147 | ||
| 148 | ||
| 3588 | 149 | (** OS related **) | 
| 2341 | 150 | |
| 3588 | 151 | (* system command execution *) | 
| 2341 | 152 | |
| 3588 | 153 | (*execute Unix command which doesn't take any input from stdin and | 
| 11078 | 154 | sends its output to stdout; could be done more easily by Unix.execute, | 
| 155 | but that function doesn't use the PATH*) | |
| 3588 | 156 | fun execute command = | 
| 157 | let | |
| 11078 | 158 | val tmp_name = OS.FileSys.tmpName (); | 
| 159 | val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); | |
| 160 | val result = TextIO.inputAll is; | |
| 161 | in | |
| 162 | TextIO.closeIn is; | |
| 163 | OS.FileSys.remove tmp_name; | |
| 164 | result | |
| 165 | end; | |
| 7855 | 166 | |
| 11078 | 167 | (*plain version; with return code*) | 
| 168 | fun system cmd = | |
| 169 | if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1; | |
| 2341 | 170 | |
| 171 | ||
| 3588 | 172 | (* getenv *) | 
| 173 | ||
| 11078 | 174 | fun getenv var = | 
| 175 | (case OS.Process.getEnv var of | |
| 176 | NONE => "" | |
| 177 | | SOME txt => txt); | |
| 15028 | 178 | |
| 179 | ||
| 15851 | 180 | (* profiling: version that works even with | 
| 15028 | 181 | ML{*profiling 1*}
 | 
| 182 | apply \\<dots> | |
| 183 | ML{*profiling 0*}
 | |
| 184 | *) | |
| 185 | ||
| 186 | val profiling: int->unit = | |
| 187 | RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler; | |
| 15699 
7d91dd712ff8
fixing an incompatibility with Posix.IO.mkTextReader
 paulson parents: 
15028diff
changeset | 188 | |
| 16374 | 189 | unless_cygwin | 
| 190 | use "ML-Systems/polyml-posix.ML"; |