| changeset 315 | de49d5780f57 |
| parent 311 | ee864694315b |
| child 316 | 74f0a06f751f |
| 314:79202e2eab6a | 315:de49d5780f57 |
|---|---|
37 *} |
37 *} |
38 |
38 |
39 ML {* |
39 ML {* |
40 fun open_file name = |
40 fun open_file name = |
41 (tracing ("Opened File: " ^ name); |
41 (tracing ("Opened File: " ^ name); |
42 file_name := SOME name) |
42 file_name := SOME name; |
43 TextIO.openOut name; ()) |
|
43 |
44 |
44 fun open_file_prelude name txt = |
45 fun open_file_prelude name txt = |
45 (open_file name; write_file (txt ^ "\n")) |
46 (open_file name; write_file (txt ^ "\n")) |
46 *} |
47 *} |
47 |
48 |