equal
deleted
inserted
replaced
17 > use "ROOT.ML"; |
17 > use "ROOT.ML"; |
18 *) |
18 *) |
19 |
19 |
20 (** ML system related **) |
20 (** ML system related **) |
21 |
21 |
22 (*proper implementation available?*) |
22 load "Obj"; |
23 fun pointer_eq (x:''a, y) = false; |
|
24 |
|
25 |
|
26 (* Poly/ML emulation *) |
|
27 |
|
28 load "Bool"; |
23 load "Bool"; |
29 load "Int"; |
24 load "Int"; |
30 load "Real"; |
25 load "Real"; |
31 load "ListPair"; |
26 load "ListPair"; |
32 load "OS"; |
27 load "OS"; |
33 load "Process"; |
28 load "Process"; |
34 load "FileSys"; |
29 load "FileSys"; |
|
30 |
|
31 (*low-level pointer equality*) |
|
32 local val cast : 'a -> int = Obj.magic |
|
33 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end; |
35 |
34 |
36 (*proper implementation available?*) |
35 (*proper implementation available?*) |
37 structure IntInf = |
36 structure IntInf = |
38 struct |
37 struct |
39 open Int; |
38 open Int; |
91 exception TimeOut |
90 exception TimeOut |
92 fun timeLimit t f x = |
91 fun timeLimit t f x = |
93 f x; |
92 f x; |
94 end; |
93 end; |
95 |
94 |
|
95 |
96 (* ML command execution *) |
96 (* ML command execution *) |
97 |
97 |
98 (*Can one redirect 'use' directly to an instream?*) |
98 (*Can one redirect 'use' directly to an instream?*) |
99 fun use_text _ _ txt = |
99 fun use_text _ _ txt = |
100 let |
100 let |