--- a/src/Pure/ML-Systems/smlnj-1.09.ML Tue Aug 05 16:22:17 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-1.09.ML Tue Aug 05 16:43:54 1997 +0200
@@ -6,20 +6,62 @@
Compatibility file for Standard ML of New Jersey, version 1.09.27 or later.
*)
-(** Poly/ML emulation **)
+(** ML system related **)
+
+(* restore old-style character / string functions *)
+
+fun ord s = Char.ord (String.sub (s, 0));
+val chr = str o Char.chr;
+val explode = (map str) o String.explode;
+val implode = String.concat;
+
+
+(* New Jersey ML parameters *)
+
+val _ =
+ (Compiler.Control.Print.printLength := 1000;
+ Compiler.Control.Print.printDepth := 350;
+ Compiler.Control.Print.stringDepth := 250;
+ Compiler.Control.Print.signatures := 2);
+
+
+(* Poly/ML emulation *)
fun quit () = exit 0;
-(*to limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
+(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
fun print_depth n =
(Compiler.Control.Print.printDepth := n div 2;
Compiler.Control.Print.printLength := n);
+(*Poly/ML-like prompts*)
Compiler.Control.primaryPrompt := "> ";
Compiler.Control.secondaryPrompt := "# ";
-(* interface for toplevel pretty printers, see also Pure/install_pp.ML *)
+(* timing *)
+
+(*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.- *)
+ val CPUtimer = Timer.startCPUTimer();
+ val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
+ val result = f();
+ val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
+ in print("User " ^ toString (usrt2-usrt1) ^
+ " GC " ^ toString (gct2-gct1) ^
+ " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
+ " secs\n")
+ handle Time => ();
+ result
+ end
+ else f ();
+
+
+(* toplevel pretty printing (see also Pure/install_pp.ML) *)
fun make_pp path pprint =
let
@@ -37,73 +79,46 @@
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
-(** New Jersey ML parameters **)
-
-val _ =
- (Compiler.Control.Print.printLength := 1000;
- Compiler.Control.Print.printDepth := 350;
- Compiler.Control.Print.stringDepth := 250;
- Compiler.Control.Print.signatures := 2);
-
-
-(** Character / string functions which are compatible with 0.93 and Poly/ML **)
-
-fun ord s = Char.ord (String.sub (s, 0));
-val chr = str o Char.chr;
-val explode = (map str) o String.explode;
-val implode = String.concat;
-
-
-(** Timing functions **)
-
-(*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.- *)
- val CPUtimer = Timer.startCPUTimer();
- val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
- val result = f();
- val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
- in print("User " ^ toString (usrt2-usrt1) ^
- " GC " ^ toString (gct2-gct1) ^
- " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
- " secs\n")
- handle Time => ();
- result
- end
- else f ();
-
-
-(** File handling **)
-
-(*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""
- | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
-
-
-(** ML command execution **)
+(* ML command execution *)
val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
-(** System command execution **)
+
+(** OS related **)
-(*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 Unix.execute, but that function
- doesn't use the PATH.*)
+(* system command execution *)
+
+(*execute Unix command which doesn't take any input from stdin and
+ sends its output to stdout; could be done more easily by Unix.execute,
+ but that function doesn't use the PATH*)
fun execute command =
- let val tmp_name = "isa_converted.tmp"
- val is = (OS.Process.system (command ^ " > " ^ tmp_name);
- TextIO.openIn tmp_name);
- val result = TextIO.inputAll is;
- in TextIO.closeIn is;
- OS.FileSys.remove tmp_name;
- result
+ let
+ val tmp_name = OS.FileSys.tmpName ();
+ val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
+ val result = TextIO.inputAll is;
+ in
+ TextIO.closeIn is;
+ OS.FileSys.remove tmp_name;
+ result
end;
-(** non-ASCII input **)
+(* file handling *)
+
+(*get time of last modification; if file doesn't exist return an empty string*)
+fun file_info "" = "" (* FIXME !? *)
+ | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
+
+
+(* getenv *)
+
+fun getenv var =
+ (case OS.Process.getEnv var of
+ NONE => ""
+ | SOME txt => txt);
+
+
+(* non-ASCII input (see also Thy/symbol_input.ML) *)
val needs_filtered_use = false;