# HG changeset patch
# User paulson
# Date 849865630 -3600
# Node ID 3eea6b72bb4fe106d911ee54e505b64e968a42d6
# Parent  55060cfeda1bb3eddade2fe3afbcf5098833863c
MLWorks compatibility: it sort of works

diff -r 55060cfeda1b -r 3eea6b72bb4f src/Pure/MLWorks.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/MLWorks.ML	Fri Dec 06 10:47:10 1996 +0100
@@ -0,0 +1,110 @@
+(*  Title:      Pure/MLWorks.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Compatibility file for MLWorks (??)
+
+NB: There is still no easy way of building Isabelle under MLWorks.  This file
+    is just a start towards compatibility.  One problem is the peculiar
+    behaviour of "use" in MLWorks.  Strange errors occur when loading theories,
+    and ROOT.ML files on subdirectories are loaded incorrectly.
+*)
+
+(*** Poly/ML emulation ***)
+
+(**
+require "system.__os";
+require "basis.__timer";
+require "system.__time";
+require "unix.__os_file_sys";
+require "basis.__list";
+require "basis.__char";
+require "basis.__string";
+require "basis.__text_io";
+**)
+
+
+(*To exit the system with an exit code -- an alternative to ^D *)
+fun exit 0 = OS.Process.exit OS.Process.success
+  | exit _ = OS.Process.exit OS.Process.failure;
+fun quit () = exit 0;
+
+(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
+fun print_depth n = ();
+
+(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
+
+fun make_pp path pprint = ();
+fun install_pp _ = ();
+
+
+(*** New Jersey ML parameters ***)
+
+(*** 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 ***)
+
+val tmpName = OS.FileSys.tmpName();
+
+(*Can one redirect 'use' directly to an instream?*)
+fun use_string slist =
+  let val tmpFile = TextIO.openOut tmpName
+  in app (fn s => TextIO.output (tmpFile, s)) slist;
+     TextIO.closeOut tmpFile;
+     use tmpName
+  end;
+
+
+(*** 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 Unix.execute, but that function
+  doesn't use the PATH.*)
+fun execute command =
+  let val is = (OS.Process.system (command ^ " > " ^ tmpName);
+                TextIO.openIn tmpName);
+      val result = TextIO.inputAll is;
+  in TextIO.closeIn is;
+     OS.FileSys.remove tmpName;
+     result
+  end;
+
+
+(*Don't know what the boolean is for*)
+fun xML filename = Shell.saveImage (filename, false);