# HG changeset patch # User wenzelm # Date 1554409057 -7200 # Node ID 25c0ad612d622bca88425f4ab052ff39dd275942 # Parent 36fb663145e5d30d1e86273e7aa24b9dc1ce8516 tuned; diff -r 36fb663145e5 -r 25c0ad612d62 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Apr 04 20:45:55 2019 +0200 +++ b/src/Pure/Pure.thy Thu Apr 04 22:17:37 2019 +0200 @@ -128,14 +128,14 @@ >> Generated_Files.generate_file_cmd); - val files_in = + val files_in_theory = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from given theories" - (Parse.and_list1 files_in >> (fn args => + (Parse.and_list1 files_in_theory >> (fn args => Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))); @@ -154,7 +154,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\compile_generated_files\ "compile generated files and export results" - (Parse.and_list files_in -- + (Parse.and_list files_in_theory -- Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", Position.none) --