use_text/file: tune text (cf. ML_Parse.fix_ints);
authorwenzelm
Sun Sep 16 14:52:34 2007 +0200 (2007-09-16)
changeset 245997b0ecf9a9055
parent 24598 44a1c0c68e21
child 24600 5877b88f262c
use_text/file: tune text (cf. ML_Parse.fix_ints);
activate proper int setup;
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Sep 16 14:52:33 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Sep 16 14:52:34 2007 +0200
     1.3 @@ -4,16 +4,12 @@
     1.4  Compatibility file for Standard ML of New Jersey 110 or later.
     1.5  *)
     1.6  
     1.7 -fun mk_int (i: int) = i;
     1.8 -fun dest_int (i: int) = i;
     1.9 -(*use "ML-Systems/proper_int.ML";*)
    1.10 -
    1.11 +use "ML-Systems/proper_int.ML";
    1.12 +use "ML-Systems/overloading_smlnj.ML";
    1.13  use "ML-Systems/exn.ML";
    1.14  use "ML-Systems/multithreading_dummy.ML";
    1.15  
    1.16  
    1.17 -(** ML system related **)
    1.18 -
    1.19  (*low-level pointer equality*)
    1.20  
    1.21  CM.autoload "$smlnj/init/init.cmi";
    1.22 @@ -40,11 +36,12 @@
    1.23  
    1.24  (* Poly/ML emulation *)
    1.25  
    1.26 +val exit = exit o dest_int;
    1.27  fun quit () = exit 0;
    1.28  
    1.29  (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
    1.30  local
    1.31 -  val depth = ref 10;
    1.32 +  val depth = ref (10: int);
    1.33  in
    1.34    fun get_print_depth () = ! depth;
    1.35    fun print_depth n =
    1.36 @@ -111,7 +108,7 @@
    1.37  
    1.38  (* ML command execution *)
    1.39  
    1.40 -fun use_text name (print, err) verbose txt =
    1.41 +fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.42    let
    1.43      val ref out_orig = Control.Print.out;
    1.44  
    1.45 @@ -122,14 +119,18 @@
    1.46        in String.substring (str, 0, Int.max (0, size str - 1)) end;
    1.47    in
    1.48      Control.Print.out := out;
    1.49 -    Backend.Interact.useStream (TextIO.openString txt) handle exn =>
    1.50 +    Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn =>
    1.51        (Control.Print.out := out_orig;
    1.52          err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.53      Control.Print.out := out_orig;
    1.54      if verbose then print (output ()) else ()
    1.55    end;
    1.56  
    1.57 -fun use_file _ _ name = use name;
    1.58 +fun use_file tune output verbose name =
    1.59 +  let
    1.60 +    val instream = TextIO.openIn name;
    1.61 +    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.62 +  in use_text tune name output verbose txt end;
    1.63  
    1.64  
    1.65