# HG changeset patch # User wenzelm # Date 1658568388 -7200 # Node ID 041d7d6339778242c99c1416dec53c974939053c # Parent fc4eaa10ec77ef7fc91e5c436b8a622b5a716155 clarified modules; diff -r fc4eaa10ec77 -r 041d7d633977 src/Pure/ROOT.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"; diff -r fc4eaa10ec77 -r 041d7d633977 src/Pure/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>\scala_build\ [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 diff -r fc4eaa10ec77 -r 041d7d633977 src/Pure/Tools/scala_build.ML --- 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>\scala_build\ [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;