tuned;
authorwenzelm
Thu, 04 Apr 2019 22:17:37 +0200
changeset 70238 25c0ad612d62
parent 70237 36fb663145e5
child 70239 0403b5127da1
tuned;
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>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
       "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>\<open>compile_generated_files\<close>
       "compile generated files and export results"
-      (Parse.and_list files_in --
+      (Parse.and_list files_in_theory --
         Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
         Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
         Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("", Position.none) --