Now declares needs_filtered_use, but still unusable with current MLWorks
authorpaulson
Wed Mar 05 10:02:53 1997 +0100 (1997-03-05)
changeset 2723f09ecc2cd3f1
parent 2722 3e07c20b967c
child 2724 ddc6cf6b62e9
Now declares needs_filtered_use, but still unusable with current MLWorks
src/Pure/MLWorks.ML
     1.1 --- a/src/Pure/MLWorks.ML	Wed Mar 05 10:01:57 1997 +0100
     1.2 +++ b/src/Pure/MLWorks.ML	Wed Mar 05 10:02:53 1997 +0100
     1.3 @@ -14,14 +14,14 @@
     1.4  (*** Poly/ML emulation ***)
     1.5  
     1.6  (**
     1.7 -require "system.__os";
     1.8 -require "basis.__timer";
     1.9 -require "system.__time";
    1.10 -require "unix.__os_file_sys";
    1.11 -require "basis.__list";
    1.12 -require "basis.__char";
    1.13 -require "basis.__string";
    1.14 -require "basis.__text_io";
    1.15 +Shell.File.loadSource "system.__os";
    1.16 +Shell.File.loadSource "basis.__timer";
    1.17 +Shell.File.loadSource "system.__time";
    1.18 +Shell.File.loadSource "unix.__os_file_sys";
    1.19 +Shell.File.loadSource "basis.__list";
    1.20 +Shell.File.loadSource "basis.__char";
    1.21 +Shell.File.loadSource "basis.__string";
    1.22 +Shell.File.loadSource "basis.__text_io";
    1.23  **)
    1.24  
    1.25  
    1.26 @@ -33,8 +33,8 @@
    1.27  (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
    1.28  fun print_depth n = ();
    1.29  
    1.30 -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.31 -
    1.32 +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML
    1.33 +  CURRENTLY UNAVAILABLE*)
    1.34  fun make_pp path pprint = ();
    1.35  fun install_pp _ = ();
    1.36  
    1.37 @@ -108,3 +108,8 @@
    1.38  
    1.39  (*Don't know what the boolean is for*)
    1.40  fun xML filename = Shell.saveImage (filename, false);
    1.41 +
    1.42 +
    1.43 +(*Non-printing and 8-bit chars are forbidden in string constants*)
    1.44 +val needs_filtered_use = true;
    1.45 +