support for Isabelle/Scala/Java modules in Isabelle/ML;

--- a/src/Pure/Pure.thy	Fri Jul 08 20:24:05 2022 +0200
+++ b/src/Pure/Pure.thy	Fri Jul 08 22:29:26 2022 +0200
@@ -24,6 +24,7 @@
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
   and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
+  and "scala_build_component" "scala_build_directory" :: 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"
@@ -189,6 +190,17 @@
             Generated_Files.compile_generated_files_cmd
               (Toplevel.context_of st) args external export export_prefix source)));
 
+  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 =>
+        Toplevel.keep (fn st => Scala_Build.scala_build_component (Toplevel.context_of st) dir)));
+
+  val _ =
+    Outer_Syntax.command \<^command_keyword>\<open>scala_build_directory\<close>
+      "build and export Isabelle/Scala/Java module (defined via build.props)"
+      (Parse.path_input >> (fn dir =>
+        Toplevel.keep (fn st => Scala_Build.scala_build_directory (Toplevel.context_of st) dir)));
 in end\<close>
 
 external_file "ROOT0.ML"

--- a/src/Pure/ROOT.ML	Fri Jul 08 20:24:05 2022 +0200
+++ b/src/Pure/ROOT.ML	Fri Jul 08 22:29:26 2022 +0200
@@ -362,4 +362,5 @@
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
-ML_file "Tools/generated_files.ML"
+ML_file "Tools/generated_files.ML";
+ML_file "Tools/scala_build.ML";

--- a/src/Pure/System/scala.scala	Fri Jul 08 20:24:05 2022 +0200
+++ b/src/Pure/System/scala.scala	Fri Jul 08 22:29:26 2022 +0200
@@ -371,6 +371,7 @@
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
+  Scala_Build.Scala_Fun,
   Base64.Decode,
   Base64.Encode,
   XZ.Compress,

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/scala_build.ML	Fri Jul 08 22:29:26 2022 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Tools/scala_build.ML
+    Author:     Makarius
+
+Build and export Isabelle/Scala/Java modules.
+*)
+
+signature SCALA_BUILD =
+sig
+  val scala_build_component: Proof.context -> Input.source -> unit
+  val scala_build_directory: Proof.context -> Input.source -> unit
+end
+
+structure Scala_Build: SCALA_BUILD =
+struct
+
+fun scala_build component ctxt dir =
+  let
+    val path = Resources.check_dir ctxt NONE dir;
+    val [jar_name, jar_bytes, output] =
+      \<^scala>\<open>scala_build\<close>
+        [Bytes.string (Value.print_bool component), Bytes.string (Path.implode path)];
+    val _ = writeln (Bytes.content output);
+  in
+    Export.export (Proof_Context.theory_of ctxt)
+      (Path.explode_binding0 (Bytes.content jar_name))
+      (Bytes.contents_blob jar_bytes)
+  end;
+
+val scala_build_component = scala_build true;
+val scala_build_directory = scala_build false;
+
+end;

--- a/src/Pure/Tools/scala_build.scala	Fri Jul 08 20:24:05 2022 +0200
+++ b/src/Pure/Tools/scala_build.scala	Fri Jul 08 22:29:26 2022 +0200
@@ -94,6 +94,24 @@
     }
   }
 
+  object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun {
+    val here = Scala_Project.here
+    def invoke(args: List[Bytes]): List[Bytes] =
+      args match {
+        case List(component, dir) =>
+          val result =
+            build_result(Path.explode(dir.text),
+              component = Value.Boolean.parse(component.text))
+          val jar_name =
+            result.jar_path match {
+              case Some(path) => path.file_name
+              case None => "result.jar"
+            }
+          List(Bytes("scala_build/" + jar_name), result.jar_bytes, Bytes(result.output))
+        case _ => error("Bad arguments")
+      }
+  }
+
   def component_contexts(): List[Context] =
     isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_))
 }