--- a/src/Pure/ML-Systems/smlnj-0.93.ML Tue Aug 05 17:01:02 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML Tue Aug 05 17:02:50 1997 +0200
@@ -6,19 +6,57 @@
Compatibility file for Standard ML of New Jersey version 0.93.
*)
-
-use"basis.ML";
+(*needs the Basis Library emulation*)
+use "basis.ML";
-(*** Poly/ML emulation ***)
+(** ML system related **)
+
+(* New Jersey ML parameters *)
+
+System.Control.Runtime.gcmessages := 0;
+
+
+(* Poly/ML emulation *)
fun quit () = exit 0;
-(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
-fun print_depth n = (System.Control.Print.printDepth := n div 2;
- System.Control.Print.printLength := n);
+(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
+fun print_depth n =
+ (System.Control.Print.printDepth := n div 2;
+ System.Control.Print.printLength := n);
+
+
+(* timing *)
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
+local
+ (*print microseconds, suppressing trailing zeroes*)
+ fun umakestring 0 = ""
+ | umakestring n =
+ chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
+in
+ (*a conditional timing function: applies f to () and, if the flag is true,
+ prints its runtime*)
+ fun cond_timeit flag f =
+ if flag then
+ let fun string_of_time (System.Timer.TIME {sec, usec}) =
+ makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
+ open System.Timer;
+ val start = start_timer()
+ val result = f();
+ val nongc = check_timer(start)
+ and gc = check_timer_gc(start);
+ val both = add_time(nongc, gc)
+ in print("Non GC " ^ string_of_time nongc ^
+ " GC " ^ string_of_time gc ^
+ " both "^ string_of_time both ^ " secs\n");
+ result
+ end
+ else f();
+end;
+
+
+(* toplevel pretty printing (see also Pure/install_pp.ML) *)
fun make_pp path pprint =
let
@@ -36,88 +74,71 @@
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
-(*** New Jersey ML parameters ***)
+(* ML command execution *)
-(* Suppresses Garbage Collection messages; default was 2 *)
-System.Control.Runtime.gcmessages := 0;
+fun use_string commands =
+ System.Compile.use_stream (open_string (implode commands));
+
-(*** Timing functions ***)
+(** OS related **)
-(*Print microseconds, suppressing trailing zeroes*)
-fun umakestring 0 = ""
- | umakestring n = chr(ord "0" + n div 100000) ^
- umakestring(10 * (n mod 100000));
+(* system command execution *)
-(*A conditional timing function: applies f to () and, if the flag is true,
- prints its runtime. *)
-fun cond_timeit flag f =
- if flag then
- let fun string_of_time (System.Timer.TIME {sec, usec}) =
- makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
- open System.Timer;
- val start = start_timer()
- val result = f();
- val nongc = check_timer(start)
- and gc = check_timer_gc(start);
- val both = add_time(nongc, gc)
- in print("Non GC " ^ string_of_time nongc ^
- " GC " ^ string_of_time gc ^
- " both "^ string_of_time both ^ " secs\n");
- result
- end
- else f();
+(*execute Unix command which doesn't take any input from stdin and
+ sends its output to stdout; could be done more easily by IO.execute,
+ but that function seems to be buggy in SML/NJ 0.93*)
+fun execute command =
+ let
+ val tmp_name = "/tmp/.isabelle-execute"; (*let's hope we win the race!*)
+ val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
+ val result = input (is, 999999);
+ in
+ close_in is;
+ System.Unsafe.SysIO.unlink tmp_name;
+ result
+ end;
-(*** File handling ***)
+(* file handling *)
(*Get time of last modification; if file doesn't exist return an empty string*)
local
- open System.Timer;
- open System.Unsafe.SysIO;
+ open System.Timer System.Unsafe.SysIO;
in
fun file_info "" = ""
- | file_info name = makestring (mtime (PATH name)) handle _ => "";
+ | file_info name = makestring (mtime (PATH name)) handle _ => "";
end;
structure OS =
- struct
+struct
structure FileSys =
- struct
- val chDir = System.Directory.cd
- val remove = System.Unsafe.SysIO.unlink (*Delete a file *)
- val getDir = System.Directory.getWD (*path of working directory*)
- end
+ struct
+ val chDir = System.Directory.cd;
+ val remove = System.Unsafe.SysIO.unlink;
+ val getDir = System.Directory.getWD;
end;
-
+end;
-(*** ML command execution ***)
-
-fun use_string commands =
- System.Compile.use_stream (open_string (implode commands));
+(*redefine to flush its output immediately -- temporary patch suggested
+ by Kim Dam Petersen*) (* FIXME !? *)
+val output = fn (s, t) => (output (s, t); flush_out s);
-(*** System command execution ***)
+(* getenv *)
-(*Execute an Unix command which doesn't take any input from stdin and
- sends its output to stdout.
- This could be done more easily by IO.execute, but that function
- seems to be buggy in SML/NJ 0.93.*)
-fun execute command =
- let val tmp_name = "isa_converted.tmp"
- val is = (System.system (command ^ " > " ^ tmp_name);
- open_in tmp_name);
- val result = input (is, 999999);
- in close_in is;
- OS.FileSys.remove tmp_name;
- result
- end;
+local
+ fun drop_last [] = []
+ | drop_last [x] = []
+ | drop_last (x :: xs) = x :: drop_last xs;
-(*redefine to flush its output immediately -- temporary patch suggested
- by Kim Dam Petersen*)
-val output = fn(s, t) => (output(s, t); flush_out s);
+ val drop_last_char = implode o drop_last o explode;
+in
+ fun getenv var = drop_last_char
+ (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
+end;
-(* symbol input *)
+(* non-ASCII input (see also Thy/symbol_input.ML) *)
val needs_filtered_use = false;
--- a/src/Pure/ML-Systems/smlnj-1.09.ML Tue Aug 05 17:01:02 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-1.09.ML Tue Aug 05 17:02:50 1997 +0200
@@ -3,7 +3,7 @@
Author: Carsten Clasohm, TU Muenchen
Copyright 1996 TU Muenchen
-Compatibility file for Standard ML of New Jersey, version 1.09.27 or later.
+Compatibility file for Standard ML of New Jersey version 1.09.27 or later.
*)
(** ML system related **)
@@ -43,7 +43,6 @@
(*a conditional timing function: applies f to () and, if the flag is true,
prints its runtime*)
-
fun cond_timeit flag f =
if flag then
let open Time (*...for Time.toString, Time.+ and Time.- *)