--- 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"
--- 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
--- 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;
--- 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