src/Pure/ML-Systems/alice.ML
changeset 24807 f66ab1dfbae1
parent 24688 a5754ca5c510
child 24809 41a21f59f74d
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Mon Oct 01 21:19:54 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Oct 01 22:29:56 2007 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  $ cd Isabelle/src/Pure
     1.5  $ env ALICE_JIT_MODE=0 alice
     1.6  - val ml_system = "alice";
     1.7 +- use "ML-Systems/exn.ML";
     1.8 +- use "ML-Systems/multithreading.ML";
     1.9 +- use "ML-Systems/time_limit.ML";
    1.10  - use "ML-Systems/alice.ML";
    1.11  - use "ROOT.ML";
    1.12  - Session.finish ();
    1.13 @@ -15,11 +18,6 @@
    1.14  
    1.15  val ml_system_fix_ints = false;
    1.16  
    1.17 -use "ML-Systems/exn.ML";
    1.18 -use "ML-Systems/multithreading.ML";
    1.19 -use "ML-Systems/time_limit.ML";
    1.20 -
    1.21 -
    1.22  fun exit 0 = (OS.Process.exit OS.Process.success): unit
    1.23    | exit _ = OS.Process.exit OS.Process.failure;
    1.24  
    1.25 @@ -29,6 +27,13 @@
    1.26  (*low-level pointer equality*)
    1.27  fun pointer_eq (_: 'a, _: 'a) = false;
    1.28  
    1.29 +(*downgraded IntInf*)
    1.30 +structure IntInf =
    1.31 +struct
    1.32 +  fun divMod (x, y) = (x div y, x mod y);
    1.33 +  open Int;
    1.34 +end;
    1.35 +
    1.36  
    1.37  (* restore old-style character / string functions *)
    1.38  
    1.39 @@ -102,9 +107,9 @@
    1.40  
    1.41  (* ML command execution *)
    1.42  
    1.43 -fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
    1.44 +fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ());
    1.45  
    1.46 -fun use_file _ _ name = use name;
    1.47 +fun use_file tune output verbose name = use name;
    1.48  
    1.49  
    1.50