121 in thy' end))); |
121 in thy' end))); |
122 |
122 |
123 val _ = |
123 val _ = |
124 Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close> |
124 Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close> |
125 "generate source file, with antiquotations" |
125 "generate source file, with antiquotations" |
126 (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) |
126 (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) |
127 >> Generated_Files.generate_file_cmd); |
127 >> Generated_Files.generate_file_cmd); |
|
128 |
|
129 val files_in = |
|
130 (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- |
|
131 Scan.option (\<^keyword>\<open>in\<close> |-- Parse.!!! Parse.theory_name); |
128 |
132 |
129 val _ = |
133 val _ = |
130 Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close> |
134 Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close> |
131 "export generated files from this or other theories" |
135 "export generated files from given theories" |
132 (Scan.repeat Parse.name_position >> (fn names => |
136 (Parse.and_list1 files_in >> (fn args => |
133 Toplevel.keep (fn st => |
137 Toplevel.keep (fn st => |
134 let |
138 Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))) |
135 val ctxt = Toplevel.context_of st; |
139 |
136 val thy = Toplevel.theory_of st; |
|
137 val other_thys = |
|
138 if null names then [thy] |
|
139 else map (Theory.check {long = false} ctxt) names; |
|
140 val paths = Generated_Files.export_files thy other_thys; |
|
141 in |
|
142 if not (null paths) then |
|
143 (writeln (Export.message thy Path.current); |
|
144 writeln (cat_lines (paths |> map (fn (path, pos) => |
|
145 Markup.markup (Markup.entityN, Position.def_properties_of pos) |
|
146 (quote (Path.implode path)))))) |
|
147 else () |
|
148 end))); |
|
149 in end\<close> |
140 in end\<close> |
150 |
141 |
151 |
142 |
152 subsection \<open>Embedded ML text\<close> |
143 subsection \<open>Embedded ML text\<close> |
153 |
144 |