# HG changeset patch
# User paulson
# Date 879760203 -3600
# Node ID 59af75feccc424fb1192c3ce885ae0af31f7e405
# Parent  85d004a96b986dad455c123d53203f7726d785ce
Updated comments.  A bug causes MLWorks to use much
more storage than necessary

diff -r 85d004a96b98 -r 59af75feccc4 src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Mon Nov 17 10:48:07 1997 +0100
+++ b/src/Pure/ML-Systems/MLWorks.ML	Mon Nov 17 10:50:03 1997 +0100
@@ -3,28 +3,21 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
-Compatibility file for MLWorks (??)
+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.
+Build Pure by typing to MLWorks (in directory Pure)
+        use "ML-Systems/MLWorks.ML";
+        use "ROOT.ML";
+	collect_as_much_as_possible ();
+	Shell.saveImage ("/anfs/bigdisc/lcp/heaps/mlworks/Pure", false);
+
+Execute saved image by typing to the shell
+	mlimage -load /anfs/bigdisc/lcp/heaps/mlworks/Pure
 *)
 
 (*** Poly/ML emulation ***)
 
-(**
-Shell.File.loadSource "system.__os";
-Shell.File.loadSource "basis.__timer";
-Shell.File.loadSource "system.__time";
-Shell.File.loadSource "unix.__os_file_sys";
-Shell.File.loadSource "basis.__list";
-Shell.File.loadSource "basis.__char";
-Shell.File.loadSource "basis.__string";
-Shell.File.loadSource "basis.__text_io";
-**)
-
-
+(*Just for versions of MLWorks that don't provide the Option structure*)
 structure Option = General;
 
 (*To exit the system with an exit code -- an alternative to ^D *)