5 |
5 |
6 Compatibility file for Moscow ML 2.00 |
6 Compatibility file for Moscow ML 2.00 |
7 |
7 |
8 NOTE: saving images does not work (yet!?), may run it interactively as follows: |
8 NOTE: saving images does not work (yet!?), may run it interactively as follows: |
9 |
9 |
10 $ cd .../Pure |
10 $ cd ~~/src/Pure |
11 $ isabelle RAW_ML_SYSTEM |
11 $ isabelle RAW_ML_SYSTEM |
12 > val ml_system = "mosml"; |
12 > val ml_system = "mosml"; |
13 > use "ML-Systems/mosml.ML"; |
13 > use "ML-Systems/mosml.ML"; |
14 > use "ROOT.ML"; |
14 > use "ROOT.ML"; |
15 *) |
15 *) |
16 |
16 |
17 (** ML system related **) |
17 (** ML system related **) |
18 |
18 |
19 |
|
20 (* Poly/ML emulation *) |
19 (* Poly/ML emulation *) |
21 |
20 |
22 load "Bool"; |
21 load "Bool"; |
23 load "Int"; |
22 load "Int"; |
24 load "Real"; |
23 load "Real"; |
25 load "ListPair"; |
24 load "ListPair"; |
26 |
|
27 load "OS"; |
25 load "OS"; |
28 load "Process"; |
26 load "Process"; |
29 load "FileSys"; |
27 load "FileSys"; |
30 |
28 |
|
29 (*proper implementation available?*) |
|
30 structure IntInf = |
|
31 struct |
|
32 open Int; |
|
33 end; |
|
34 |
|
35 structure Real = |
|
36 struct |
|
37 open Real; |
|
38 val realFloor = real o floor; |
|
39 end; |
|
40 |
|
41 structure Time = |
|
42 struct |
|
43 open Time; |
|
44 fun toString t = Time.toString t |
|
45 handle Overflow => Real.toString (Time.toReal t); (*workaround Y2004 bug*) |
|
46 end; |
|
47 |
31 structure OS = |
48 structure OS = |
32 struct |
49 struct |
33 open OS |
50 open OS |
34 structure Process = Process |
51 structure Process = Process |
35 structure FileSys = FileSys |
52 structure FileSys = FileSys |
36 end; |
53 end; |
37 |
54 |
38 (*To exit the system with an exit code -- an alternative to ^D *) |
|
39 fun exit 0 = Process.exit Process.success |
|
40 | exit _ = Process.exit Process.failure; |
|
41 |
|
42 (*limit the printing depth*) |
55 (*limit the printing depth*) |
43 fun print_depth n = |
56 fun print_depth n = |
44 (Meta.printDepth := n div 2; |
57 (Meta.printDepth := n div 2; |
45 Meta.printLength := n); |
58 Meta.printLength := n); |
46 |
59 |