src/Pure/NJ.ML

--- a/src/Pure/NJ.ML	Tue Feb 06 12:42:31 1996 +0100
+++ b/src/Pure/NJ.ML	Tue Feb 06 12:44:31 1996 +0100
@@ -6,42 +6,19 @@
 Compatibility file for Standard ML of New Jersey.
 *)
 
-(*** Poly/ML emulation ***)
 
-(*To exit the system with an exit code -- an alternative to ^D *)
-val exit = System.Unsafe.CInterface.exit;
-fun quit () = exit 0;
+(*Determine if we are running under 0.93 or a newer version of SML/NJ
+  This is based on the variable "version" defined in 0.93's System structure
+  which is no longer present in 1.09.*)
 
-(*To change the current directory*)
-val cd = System.Directory.cd;
+local val version = ""; open System in
+  val smlversion = if version <> "" then 93 else 109
+end;
 
-(*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);
+use (if smlversion = 93 then "NJ093.ML" else "NJ1xx.ML");
 
 
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp path pprint =
-  let
-    open System.PrettyPrint;
-
-    fun pp pps obj =
-      pprint obj
-        (add_string pps, begin_block pps INCONSISTENT,
-          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
-          fn () => end_block pps);
-  in
-    (path, pp)
-  end;
-
-fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
-
-
-(*** New Jersey ML parameters ***)
-
-(* Suppresses Garbage Collection messages;  default was 2 *)
-System.Control.Runtime.gcmessages := 0;
+(** Other functions which are not specific to 0.93 or 1.xx*)
 
 (*redefine to flush its output immediately -- temporary patch suggested
   by Kim Dam Petersen*)
@@ -49,72 +26,3 @@
 
 (*Dummy version of the Poly/ML function*)
 fun commit() = ();
-
-(*For use in Makefiles -- saves space*)
-fun xML filename banner = (exportML filename;  print(banner^"\n"));
-
-(*** Timing functions ***)
-
-(*Print microseconds, suppressing trailing zeroes*)
-fun umakestring 0 = ""
-  | umakestring n = chr(ord"0" + n div 100000) ^
-                    umakestring(10 * (n mod 100000));
-
-(*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();
-
-
-(*** File handling ***)
-
-(*Get time of last modification.*)
-local
-    open System.Timer;
-    open System.Unsafe.SysIO;
-in
-  fun file_info "" = ""
-    | file_info name = makestring (mtime (PATH name));
-
-  val delete_file = unlink;
-end;
-
-(*Get pathname of current working directory *)
-fun pwd () = System.Directory.getWD ();
-
-
-(*** ML command execution ***)
-
-fun use_string commands = 
-  System.Compile.use_stream (open_string (implode commands));
-
-
-(*** System command execution ***)
-
-(*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;
-     delete_file tmp_name;
-     result
-  end;