clarified modules;
authorwenzelm
Sat, 23 Jul 2022 11:26:28 +0200
changeset 75691 041d7d633977
parent 75690 fc4eaa10ec77
child 75692 048bbe0bf807
clarified modules;
src/Pure/ROOT.ML
src/Pure/Tools/generated_files.ML
src/Pure/Tools/scala_build.ML
--- a/src/Pure/ROOT.ML	Fri Jul 22 16:41:41 2022 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 23 11:26:28 2022 +0200
@@ -363,5 +363,4 @@
 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";
--- a/src/Pure/Tools/generated_files.ML	Fri Jul 22 16:41:41 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Sat Jul 23 11:26:28 2022 +0200
@@ -304,7 +304,14 @@
       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 ctxt dir end);
+      val [jar_name, jar_bytes, output] =
+        \<^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)
+        (Path.explode_binding0 (Bytes.content jar_name))
+        (Bytes.contents_blob jar_bytes)
+    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 16:41:41 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      Pure/Tools/scala_build.ML
-    Author:     Makarius
-
-Build and export Isabelle/Scala/Java modules.
-*)
-
-signature SCALA_BUILD =
-sig
-  val scala_build: Proof.context -> Path.T -> unit
-end
-
-structure Scala_Build: SCALA_BUILD =
-struct
-
-fun scala_build ctxt dir =
-  let
-    val [jar_name, jar_bytes, output] =
-      \<^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)
-      (Path.explode_binding0 (Bytes.content jar_name))
-      (Bytes.contents_blob jar_bytes)
-  end;
-
-end;