equal
deleted
inserted
replaced
26 setup {* setup_filename *} |
26 setup {* setup_filename *} |
27 |
27 |
28 ML {* |
28 ML {* |
29 fun write_file txt thy = |
29 fun write_file txt thy = |
30 let |
30 let |
31 val stream = Config.get_thy thy filename |
31 val stream = Config.get_global thy filename |
32 |> TextIO.openAppend |
32 |> TextIO.openAppend |
33 in |
33 in |
34 TextIO.output (stream, txt); |
34 TextIO.output (stream, txt); |
35 TextIO.flushOut stream; (* needed ?*) |
35 TextIO.flushOut stream; (* needed ?*) |
36 TextIO.closeOut stream |
36 TextIO.closeOut stream |
71 fun open_file name thy = |
71 fun open_file name thy = |
72 let |
72 let |
73 val _ = tracing ("Open File: " ^ name) |
73 val _ = tracing ("Open File: " ^ name) |
74 val _ = TextIO.openOut name |
74 val _ = TextIO.openOut name |
75 in |
75 in |
76 Config.put_thy filename name thy |
76 Config.put_global filename name thy |
77 end |
77 end |
78 *} |
78 *} |
79 |
79 |
80 ML {* |
80 ML {* |
81 fun open_file_with_prelude name txts thy = |
81 fun open_file_with_prelude name txts thy = |