--- a/src/Pure/Pure.thy Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Pure/Pure.thy Tue Jan 15 20:03:53 2019 +0100
@@ -22,6 +22,7 @@
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "external_file" "bibtex_file" :: thy_load
and "generate_file" :: thy_decl
+ and "export_generated_files" :: diag
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
@@ -125,6 +126,26 @@
(Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
>> Generated_Files.generate_file_cmd);
+ val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
+ "export generated files from this or other theories"
+ (Scan.repeat Parse.name_position >> (fn names =>
+ Toplevel.keep (fn st =>
+ let
+ val ctxt = Toplevel.context_of st;
+ val thy = Toplevel.theory_of st;
+ val other_thys =
+ if null names then [thy]
+ else map (Theory.check {long = false} ctxt) names;
+ val paths = Generated_Files.export_files thy other_thys;
+ in
+ if not (null paths) then
+ (writeln (Export.message thy "");
+ writeln (cat_lines (paths |> map (fn (path, pos) =>
+ Markup.markup (Markup.entityN, Position.def_properties_of pos)
+ (quote (Path.implode path))))))
+ else ()
+ end)));
in end\<close>
--- a/src/Pure/Tools/generated_files.ML Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Pure/Tools/generated_files.ML Tue Jan 15 20:03:53 2019 +0100
@@ -7,9 +7,9 @@
signature GENERATED_FILES =
sig
val add_files: (Path.T * Position.T) * string -> theory -> theory
- val get_files: theory -> (Path.T * string) list
- val write_files: theory -> Path.T -> Path.T list
- val export_files: theory -> Path.T list
+ val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
+ val write_files: theory -> Path.T -> (Path.T * Position.T) list
+ val export_files: theory -> theory list -> (Path.T * Position.T) list
type file_type =
{name: string, ext: string, make_comment: string -> string, make_string: string -> string}
val file_type:
@@ -67,18 +67,21 @@
| NONE => (path, (pos, text)) :: files))
end;
-val get_files = map (apsnd #2) o rev o #1 o Data.get;
+val get_files =
+ map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
fun write_files thy dir =
- get_files thy |> map (fn (path, text) =>
+ get_files thy |> map (fn {path, pos, text} =>
let
val path' = Path.expand (Path.append dir path);
val _ = Isabelle_System.mkdirs (Path.dir path');
val _ = File.generate path' text;
- in path end);
+ in (path, pos) end);
-fun export_files thy =
- get_files thy |> map (fn (path, text) => (Export.export thy (Path.implode path) [text]; path));
+fun export_files thy other_thys =
+ other_thys |> maps (fn other_thy =>
+ get_files other_thy |> map (fn {path, pos, text} =>
+ (Export.export thy (Path.implode path) [text]; (path, pos))));
(* file types *)
--- a/src/Tools/Haskell/Haskell.thy Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Tools/Haskell/Haskell.thy Tue Jan 15 20:03:53 2019 +0100
@@ -1924,6 +1924,6 @@
return ()
\<close>
-ML_command \<open>Generated_Files.export_files \<^theory>\<close>
+export_generated_files
end
--- a/src/Tools/Haskell/Test.thy Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Tools/Haskell/Test.thy Tue Jan 15 20:03:53 2019 +0100
@@ -14,7 +14,7 @@
val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
val modules = files
- |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
+ |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
val _ =
GHC.new_project tmp_dir
{name = "isabelle",