# HG changeset patch
# User paulson
# Date 857552573 -3600
# Node ID f09ecc2cd3f1fef1881b6005eebca9f5a4ab7a43
# Parent  3e07c20b967c5b95376eae798fbdd6c65aa70fc6
Now declares needs_filtered_use, but still unusable with current MLWorks

diff -r 3e07c20b967c -r f09ecc2cd3f1 src/Pure/MLWorks.ML
--- a/src/Pure/MLWorks.ML	Wed Mar 05 10:01:57 1997 +0100
+++ b/src/Pure/MLWorks.ML	Wed Mar 05 10:02:53 1997 +0100
@@ -14,14 +14,14 @@
 (*** 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";
+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";
 **)
 
 
@@ -33,8 +33,8 @@
 (*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*)
-
+(*Interface for toplevel pretty printers, see also Pure/install_pp.ML
+  CURRENTLY UNAVAILABLE*)
 fun make_pp path pprint = ();
 fun install_pp _ = ();
 
@@ -108,3 +108,8 @@
 
 (*Don't know what the boolean is for*)
 fun xML filename = Shell.saveImage (filename, false);
+
+
+(*Non-printing and 8-bit chars are forbidden in string constants*)
+val needs_filtered_use = true;
+