# HG changeset patch
# User wenzelm
# Date 1658495726 -7200
# Node ID 42f19e398ee436a0673389a09a847bd997f09e05
# Parent  07cd3b243c6900edecd63bbc2f97123c14f50a65
command 'scala_build_generated_files' with proper management of source dependencies;
support more file-formats;

diff -r 07cd3b243c69 -r 42f19e398ee4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Jul 21 15:01:48 2022 +0200
+++ b/src/Pure/Pure.thy	Fri Jul 22 15:15:26 2022 +0200
@@ -23,6 +23,7 @@
   and "external_file" "bibtex_file" "ROOTS_file" :: thy_load
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
+  and "scala_build_generated_files" :: diag
   and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
   and "export_classpath"
   and "scala_build_component" "scala_build_directory" :: diag
@@ -192,6 +193,16 @@
               (Toplevel.context_of st) args external export export_prefix source)));
 
   val _ =
+    Outer_Syntax.command \<^command_keyword>\<open>scala_build_generated_files\<close>
+      "build and export Isabelle/Scala/Java module"
+      (Parse.and_list files_in_theory --
+        Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) []
+        >> (fn (args, external) =>
+          Toplevel.keep (fn st =>
+            Generated_Files.scala_build_generated_files_cmd
+              (Toplevel.context_of st) args external)));
+
+  val _ =
     Outer_Syntax.command \<^command_keyword>\<open>scala_build_component\<close>
       "build and export Isabelle/Scala/Java module (defined via etc/build.props)"
       (Parse.path_input >> (fn dir =>
diff -r 07cd3b243c69 -r 42f19e398ee4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 21 15:01:48 2022 +0200
+++ b/src/Pure/ROOT.ML	Fri Jul 22 15:15:26 2022 +0200
@@ -363,5 +363,5 @@
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
+ML_file "Tools/scala_build.ML";
 ML_file "Tools/generated_files.ML";
-ML_file "Tools/scala_build.ML";
diff -r 07cd3b243c69 -r 42f19e398ee4 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Thu Jul 21 15:01:48 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Fri Jul 22 15:15:26 2022 +0200
@@ -36,6 +36,11 @@
   val check_external_files: Proof.context ->
     Input.source list * Input.source -> Path.T list * Path.T
   val get_external_files: Path.T -> Path.T list * Path.T -> unit
+  val scala_build_generated_files: Proof.context -> (Path.binding list * theory) list ->
+    (Path.T list * Path.T) list -> unit
+  val scala_build_generated_files_cmd: Proof.context ->
+    ((string * Position.T) list * (string * Position.T) option) list ->
+    (Input.source list * Input.source) list -> unit
   val with_compile_dir: (Path.T -> unit) -> unit
   val compile_generated_files: Proof.context ->
     (Path.binding list * theory) list ->
@@ -290,6 +295,23 @@
   files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir);
 
 
+(* scala_build_generated_files *)
+
+fun scala_build_generated_files ctxt args external =
+  Isabelle_System.with_tmp_dir "scala_build" (fn dir =>
+    let
+      val files = maps get_files_in args;
+      val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
+      val _ = List.app (write_file dir o #1) files;
+      val _ = List.app (get_external_files dir) external;
+    in Scala_Build.scala_build_directory ctxt (Input.string (Path.implode (Path.expand dir))) end);
+
+fun scala_build_generated_files_cmd ctxt args external =
+  scala_build_generated_files ctxt
+    (map (check_files_in ctxt) args)
+    (map (check_external_files ctxt) external)
+
+
 (* compile_generated_files *)
 
 val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
@@ -369,7 +391,11 @@
      file_type \<^binding>\<open>Scala\<close>
       {ext = "scala",
        make_comment = enclose "/*" "*/",
-       make_string = Java.print_string});
+       make_string = Java.print_string} #>
+     file_type \<^binding>\<open>Properties\<close>
+      {ext = "props",
+       make_comment = enclose "#" "",
+       make_string = I});