equal
deleted
inserted
replaced
18 (* re-definition of various ML antiquotations *) |
18 (* re-definition of various ML antiquotations *) |
19 (* to have a special tag for text enclosed in ML; *) |
19 (* to have a special tag for text enclosed in ML; *) |
20 (* they also write the code into a separate file *) |
20 (* they also write the code into a separate file *) |
21 |
21 |
22 ML {* |
22 ML {* |
23 val (filename, setup_filename) = Attrib.config_string "filename" "File_Code.ML" |
23 val (filename, setup_filename) = Attrib.config_string "filename" (K "File_Code.ML") |
24 *} |
24 *} |
25 |
25 |
26 setup {* setup_filename *} |
26 setup {* setup_filename *} |
27 |
27 |
28 ML {* |
28 ML {* |