equal
deleted
inserted
replaced
13 (* re-definition of various ML antiquotations *) |
13 (* re-definition of various ML antiquotations *) |
14 (* to have a special tag for text enclosed in ML; *) |
14 (* to have a special tag for text enclosed in ML; *) |
15 (* they also write the code into a separate file *) |
15 (* they also write the code into a separate file *) |
16 |
16 |
17 ML {* |
17 ML {* |
18 val (filename, setup_filename) = Attrib.config_string "filename" (K "File_Code.ML") |
18 val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML") |
19 *} |
19 *} |
20 |
20 |
21 setup {* setup_filename *} |
|
22 |
21 |
23 ML {* |
22 ML {* |
24 fun write_file txt thy = |
23 fun write_file txt thy = |
25 let |
24 let |
26 val stream = Config.get_global thy filename |
25 val stream = Config.get_global thy filename |