equal
deleted
inserted
replaced
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 > Session.finish (); |
15 > Session.finish (); |
16 > cd "../FOL"; |
16 > cd "../FOL"; |
|
17 > use "ROOT.ML"; |
|
18 > Session.finish (); |
|
19 > cd "../ZF"; |
17 > use "ROOT.ML"; |
20 > use "ROOT.ML"; |
18 *) |
21 *) |
19 |
22 |
20 (** ML system related **) |
23 (** ML system related **) |
21 |
24 |
41 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end; |
44 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end; |
42 |
45 |
43 (*proper implementation available?*) |
46 (*proper implementation available?*) |
44 structure IntInf = |
47 structure IntInf = |
45 struct |
48 struct |
|
49 fun divMod (x, y) = (x div y, x mod y); |
46 open Int; |
50 open Int; |
47 end; |
51 end; |
48 |
52 |
49 structure Real = |
53 structure Real = |
50 struct |
54 struct |
143 |
147 |
144 |
148 |
145 (* ML command execution *) |
149 (* ML command execution *) |
146 |
150 |
147 (*Can one redirect 'use' directly to an instream?*) |
151 (*Can one redirect 'use' directly to an instream?*) |
148 fun use_text _ _ _ txt = |
152 fun use_text (tune: string -> string) _ _ _ txt = |
149 let |
153 let |
150 val tmp_name = FileSys.tmpName (); |
154 val tmp_name = FileSys.tmpName (); |
151 val tmp_file = TextIO.openOut tmp_name; |
155 val tmp_file = TextIO.openOut tmp_name; |
152 in |
156 in |
153 TextIO.output (tmp_file, txt); |
157 TextIO.output (tmp_file, tune txt); |
154 TextIO.closeOut tmp_file; |
158 TextIO.closeOut tmp_file; |
155 use tmp_name; |
159 use tmp_name; |
156 FileSys.remove tmp_name |
160 FileSys.remove tmp_name |
157 end; |
161 end; |
158 |
162 |
159 fun use_file _ _ name = use name; |
163 fun use_file _ _ _ name = use name; |
160 |
164 |
161 |
165 |
162 |
166 |
163 (** interrupts **) (*Note: may get into race conditions*) |
167 (** interrupts **) (*Note: may get into race conditions*) |
164 |
168 |