1.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML Fri Jun 04 11:51:31 2004 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,195 +0,0 @@
1.4 -(* Title: Pure/ML-Systems/smlnj-0.93.ML
1.5 - ID: $Id$
1.6 - Author: Carsten Clasohm, TU Muenchen
1.7 - Copyright 1996 TU Muenchen
1.8 -
1.9 -Compatibility file for Standard ML of New Jersey version 0.93.
1.10 -*)
1.11 -
1.12 -(*needs the Basis Library emulation*)
1.13 -use "basis.ML";
1.14 -
1.15 -structure String =
1.16 -struct
1.17 - fun substring args = String.substring args
1.18 - handle String.Substring => raise Subscript;
1.19 - fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
1.20 - handle Subscript => false;
1.21 - fun str (s : string) = s;
1.22 - fun translate f s = implode (map f (explode s));
1.23 -end;
1.24 -
1.25 -
1.26 -
1.27 -(** ML system related **)
1.28 -
1.29 -(* New Jersey ML parameters *)
1.30 -
1.31 -System.Control.Runtime.gcmessages := 0;
1.32 -
1.33 -
1.34 -(* Poly/ML emulation *)
1.35 -
1.36 -fun quit () = exit 0;
1.37 -
1.38 -(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
1.39 -fun print_depth n =
1.40 - (System.Control.Print.printDepth := n div 2;
1.41 - System.Control.Print.printLength := n);
1.42 -
1.43 -
1.44 -
1.45 -(* timing *)
1.46 -
1.47 -(*Note start point for timing*)
1.48 -fun startTiming() = System.Timer.start_timer();
1.49 -
1.50 -(*Finish timing and return string*)
1.51 -local
1.52 - (*print microseconds, suppressing trailing zeroes*)
1.53 - fun umakestring 0 = ""
1.54 - | umakestring n =
1.55 - chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
1.56 -
1.57 - fun string_of_time (System.Timer.TIME {sec, usec}) =
1.58 - makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
1.59 -
1.60 -in
1.61 -
1.62 -fun endTiming start =
1.63 - let val nongc = System.Timer.check_timer(start)
1.64 - and gc = System.Timer.check_timer_gc(start);
1.65 - val both = System.Timer.add_time(nongc, gc)
1.66 - in "Non GC " ^ string_of_time nongc ^
1.67 - " GC " ^ string_of_time gc ^
1.68 - " both "^ string_of_time both ^ " secs\n"
1.69 - end
1.70 -end;
1.71 -
1.72 -
1.73 -(* prompts *)
1.74 -
1.75 -fun ml_prompts p1 p2 = ();
1.76 -
1.77 -
1.78 -(* toplevel pretty printing (see also Pure/install_pp.ML) *)
1.79 -
1.80 -fun make_pp path pprint =
1.81 - let
1.82 - open System.PrettyPrint;
1.83 -
1.84 - fun pp pps obj =
1.85 - pprint obj
1.86 - (add_string pps, begin_block pps INCONSISTENT,
1.87 - fn wd => add_break pps (wd, 0), fn () => add_newline pps,
1.88 - fn () => end_block pps);
1.89 - in
1.90 - (path, pp)
1.91 - end;
1.92 -
1.93 -fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
1.94 -
1.95 -
1.96 -(* ML command execution *)
1.97 -
1.98 -fun use_text _ _ = System.Compile.use_stream o open_string;
1.99 -
1.100 -
1.101 -
1.102 -(** interrupts **)
1.103 -
1.104 -exception Interrupt;
1.105 -
1.106 -local
1.107 -
1.108 -fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
1.109 -
1.110 -fun release NONE = ()
1.111 - | release (SOME exn) = raise exn;
1.112 -
1.113 -structure Signals = System.Signals;
1.114 -
1.115 -in
1.116 -
1.117 -fun ignore_interrupt f x =
1.118 - let
1.119 - val old_handler = Signals.inqHandler Signals.SIGINT;
1.120 - val _ = Signals.setHandler (Signals.SIGINT, SOME #2);
1.121 - val result = capture f x;
1.122 - val _ = Signals.setHandler (Signals.SIGINT, old_handler);
1.123 - in release result end;
1.124 -
1.125 -fun raise_interrupt f x =
1.126 - let
1.127 - val interrupted = ref false;
1.128 - val result = ref NONE;
1.129 - val old_handler = Signals.inqHandler Signals.SIGINT;
1.130 - in
1.131 - callcc (fn cont =>
1.132 - (Signals.setHandler (Signals.SIGINT, SOME (fn _ => (interrupted := true; cont)));
1.133 - result := capture f x));
1.134 - Signals.setHandler (Signals.SIGINT, old_handler);
1.135 - if ! interrupted then raise Interrupt else release (! result)
1.136 - end;
1.137 -
1.138 -end;
1.139 -
1.140 -
1.141 -(** OS related **)
1.142 -
1.143 -(* system command execution *)
1.144 -
1.145 -(*execute Unix command which doesn't take any input from stdin and
1.146 - sends its output to stdout; could be done more easily by IO.execute,
1.147 - but that function seems to be buggy in SML/NJ 0.93*)
1.148 -fun execute command =
1.149 - let
1.150 - val tmp_name = "/tmp/isabelle-execute";
1.151 - val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
1.152 - val result = input (is, 999999);
1.153 - in
1.154 - close_in is;
1.155 - System.Unsafe.SysIO.unlink tmp_name;
1.156 - result
1.157 - end;
1.158 -
1.159 -(*plain version; with return code*)
1.160 -fun system cmd = System.system cmd div 256;
1.161 -
1.162 -
1.163 -(* file handling *)
1.164 -
1.165 -(*get time of last modification*)
1.166 -local
1.167 - open System.Timer System.Unsafe.SysIO;
1.168 -in
1.169 - fun file_info name = makestring (mtime (PATH name)) handle _ => "";
1.170 -end;
1.171 -
1.172 -structure OS =
1.173 -struct
1.174 - structure FileSys =
1.175 - struct
1.176 - val chDir = System.Directory.cd;
1.177 - val remove = System.Unsafe.SysIO.unlink;
1.178 - val getDir = System.Directory.getWD;
1.179 - end;
1.180 -end;
1.181 -
1.182 -(*redefine to flush its output immediately -- temporary patch suggested
1.183 - by Kim Dam Petersen*) (* FIXME !? *)
1.184 -val output = fn (s, t) => (output (s, t); flush_out s);
1.185 -
1.186 -
1.187 -(* getenv *)
1.188 -
1.189 -local
1.190 - fun drop_last [] = []
1.191 - | drop_last [x] = []
1.192 - | drop_last (x :: xs) = x :: drop_last xs;
1.193 -
1.194 - val drop_last_char = implode o drop_last o explode;
1.195 -in
1.196 - fun getenv var = drop_last_char
1.197 - (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
1.198 -end;