# HG changeset patch
# User wenzelm
# Date 1658496536 -7200
# Node ID c8dc5d1adc7bfb3b39619d21ce832811d1de057f
# Parent  42f19e398ee436a0673389a09a847bd997f09e05
removed obsolete commands;

diff -r 42f19e398ee4 -r c8dc5d1adc7b src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jul 22 15:15:26 2022 +0200
+++ b/src/Pure/Pure.thy	Fri Jul 22 15:28:56 2022 +0200
@@ -26,7 +26,6 @@
   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
   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"
@@ -201,18 +200,6 @@
           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 =>
-        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"
diff -r 42f19e398ee4 -r c8dc5d1adc7b src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jul 22 15:15:26 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Fri Jul 22 15:28:56 2022 +0200
@@ -304,7 +304,7 @@
       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);
+    in Scala_Build.scala_build ctxt dir end);
 
 fun scala_build_generated_files_cmd ctxt args external =
   scala_build_generated_files ctxt
diff -r 42f19e398ee4 -r c8dc5d1adc7b src/Pure/Tools/scala_build.ML
--- a/src/Pure/Tools/scala_build.ML	Fri Jul 22 15:15:26 2022 +0200
+++ b/src/Pure/Tools/scala_build.ML	Fri Jul 22 15:28:56 2022 +0200
@@ -6,19 +6,16 @@
 
 signature SCALA_BUILD =
 sig
-  val scala_build_component: Proof.context -> Input.source -> unit
-  val scala_build_directory: Proof.context -> Input.source -> unit
+  val scala_build: Proof.context -> Path.T -> unit
 end
 
 structure Scala_Build: SCALA_BUILD =
 struct
 
-fun scala_build component ctxt dir =
+fun scala_build 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)];
+      \<^scala>\<open>scala_build\<close> [Bytes.string (Isabelle_System.absolute_path dir)];
     val _ = writeln (Bytes.content output);
   in
     Export.export (Proof_Context.theory_of ctxt)
@@ -26,7 +23,4 @@
       (Bytes.contents_blob jar_bytes)
   end;
 
-val scala_build_component = scala_build true;
-val scala_build_directory = scala_build false;
-
 end;
diff -r 42f19e398ee4 -r c8dc5d1adc7b src/Pure/Tools/scala_build.scala
--- a/src/Pure/Tools/scala_build.scala	Fri Jul 22 15:15:26 2022 +0200
+++ b/src/Pure/Tools/scala_build.scala	Fri Jul 22 15:28:56 2022 +0200
@@ -98,10 +98,8 @@
     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))
+        case List(dir) =>
+          val result = build_result(Path.explode(dir.text))
           val jar_name =
             result.jar_path match {
               case Some(path) => path.file_name