--- a/src/Doc/Isar_Ref/Spec.thy Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Jul 22 16:41:41 2022 +0200
@@ -1320,6 +1320,16 @@
browsed via the virtual file-system with prefix ``\<^verbatim>\<open>isabelle-export:\<close>''
(using the regular file-browser).
+ \<^descr> \<^theory_text>\<open>scala_build_generated_files paths (in thy)\<close> retrieves named generated
+ files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into a temporary
+ directory, which is taken as starting point for build process of
+ Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The
+ corresponding @{path build.props} file is expected directly in the toplevel
+ directory, instead of @{path "etc/build.props"} for Isabelle system
+ components. These properties need to specify sources, resources, services
+ etc. as usual. The resulting \<^verbatim>\<open>jar\<close> module becomes an export artifact of the
+ session database.
+
\<^descr> \<^theory_text>\<open>compile_generated_files paths (in thy) where compile_body\<close> retrieves
named generated files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into
a temporary directory, such that the \<open>compile_body\<close> may operate on them as
--- a/src/Doc/System/Scala.thy Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Doc/System/Scala.thy Fri Jul 22 16:41:41 2022 +0200
@@ -256,7 +256,7 @@
Option \<^verbatim>\<open>-q\<close> suppresses all output on stdout/stderr produced by the Scala or
Java compiler.
- \<^medskip> Explicit invocation of \<^verbatim>\<open>isabelle scala_build\<close> mainly serves testing or
+ \<^medskip> Explicit invocation of @{tool scala_build} mainly serves testing or
applications with special options: the Isabelle system normally does an
automatic the build on demand.
\<close>
--- a/src/Pure/General/file.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/General/file.scala Fri Jul 22 16:41:41 2022 +0200
@@ -296,17 +296,18 @@
/* content */
object Content {
- def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content)
- def apply(path: Path, content: String): Content = new Content_String(path, content)
+ def apply(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
+ def apply(path: Path, content: String): Content_String = new Content_String(path, content)
def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
}
trait Content {
def path: Path
def write(dir: Path): Unit
+ override def toString: String = path.toString
}
- final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content {
+ final class Content_Bytes private[File](val path: Path, val content: Bytes) extends Content {
def write(dir: Path): Unit = {
val full_path = dir + path
Isabelle_System.make_directory(full_path.expand.dir)
@@ -314,7 +315,7 @@
}
}
- final class Content_String private[File](val path: Path, content: String) extends Content {
+ final class Content_String private[File](val path: Path, val content: String) extends Content {
def write(dir: Path): Unit = {
val full_path = dir + path
Isabelle_System.make_directory(full_path.expand.dir)
@@ -322,7 +323,7 @@
}
}
- final class Content_XML private[File](val path: Path, content: XML.Body) {
+ final class Content_XML private[File](val path: Path, val content: XML.Body) {
def output(out: XML.Body => String): Content_String =
new Content_String(path, out(content))
}
--- a/src/Pure/Pure.thy Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Pure.thy Fri Jul 22 16:41:41 2022 +0200
@@ -23,8 +23,9 @@
and "external_file" "bibtex_file" "ROOTS_file" :: thy_load
and "generate_file" :: thy_decl
and "export_generated_files" :: diag
+ and "scala_build_generated_files" :: diag
and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
- and "scala_build_component" "scala_build_directory" :: diag
+ and "export_classpath"
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"
@@ -191,16 +192,14 @@
(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)));
+ Outer_Syntax.command \<^command_keyword>\<open>scala_build_generated_files\<close>
+ "build and export Isabelle/Scala/Java module"
+ (Parse.and_list files_in_theory --
+ Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) []
+ >> (fn (args, external) =>
+ Toplevel.keep (fn st =>
+ Generated_Files.scala_build_generated_files_cmd
+ (Toplevel.context_of st) args external)));
in end\<close>
external_file "ROOT0.ML"
--- a/src/Pure/ROOT.ML Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/ROOT.ML Fri Jul 22 16:41:41 2022 +0200
@@ -297,6 +297,7 @@
(*Isabelle system*)
ML_file "PIDE/protocol_command.ML";
+ML_file "System/java.ML";
ML_file "System/scala.ML";
ML_file "System/process_result.ML";
ML_file "System/isabelle_system.ML";
@@ -362,5 +363,5 @@
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";
-ML_file "Tools/scala_build.ML";
--- a/src/Pure/System/isabelle_system.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/System/isabelle_system.scala Fri Jul 22 16:41:41 2022 +0200
@@ -55,7 +55,7 @@
/* init settings + services */
- def make_services(): List[Class[Service]] = {
+ def get_services(): List[Class[Service]] = {
def make(where: String, names: List[String]): List[Class[Service]] = {
for (name <- names) yield {
def err(msg: String): Nothing =
@@ -75,12 +75,12 @@
make(quote(platform_jar),
isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList)
- from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar)
+ from_env("ISABELLE_SCALA_SERVICES") ::: Scala.get_classpath().flatMap(from_jar)
}
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
isabelle.setup.Environment.init(isabelle_root, cygwin_root)
- synchronized { if (_services.isEmpty) { _services = Some(make_services()) } }
+ synchronized { if (_services.isEmpty) { _services = Some(get_services()) } }
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/java.ML Fri Jul 22 16:41:41 2022 +0200
@@ -0,0 +1,42 @@
+(* Title: Pure/System/java.ML
+ Author: Makarius
+
+Support for Java language.
+*)
+
+signature JAVA =
+sig
+ val print_string: string -> string
+end;
+
+structure Java: JAVA =
+struct
+
+(* string literals *)
+
+local
+
+val print_str =
+ fn "\b" => "\\b"
+ | "\t" => "\\t"
+ | "\n" => "\\n"
+ | "\f" => "\\f"
+ | "\r" => "\\r"
+ | "\"" => "\\\""
+ | "\\" => "\\\\"
+ | s =>
+ let val c = ord s in
+ if c < 16 then "\\u000" ^ Int.fmt StringCvt.HEX c
+ else if c < 128 then "\\u00" ^ Int.fmt StringCvt.HEX c
+ else error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote s)
+ end;
+
+in
+
+fun print_string str =
+ quote (translate_string print_str str)
+ handle Fail _ => error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote str);
+
+end;
+
+end;
--- a/src/Pure/System/scala.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/System/scala.scala Fri Jul 22 16:41:41 2022 +0200
@@ -100,7 +100,7 @@
/** compiler **/
- def class_path(): List[String] =
+ def get_classpath(): List[String] =
space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
.filter(_.nonEmpty)
@@ -172,7 +172,7 @@
File.find_files(dir, file => file.getName.endsWith(".jar")).
map(File.absolute_name)
- val classpath = (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+ val classpath = (get_classpath() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
val settings1 = isabelle_settings ::: settings ::: List("-classpath", classpath)
new Context(settings1, class_loader)
}
--- a/src/Pure/Thy/document_build.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Thy/document_build.scala Fri Jul 22 16:41:41 2022 +0200
@@ -121,10 +121,12 @@
db_context: Sessions.Database_Context,
progress: Progress = new Progress
): Context = {
- val info = deps.sessions_structure(session)
+ val structure = deps.sessions_structure
+ val info = structure(session)
val base = deps(session)
val hierarchy = deps.sessions_structure.build_hierarchy(session)
- new Context(info, base, hierarchy, db_context, progress)
+ val classpath = db_context.get_classpath(structure, session)
+ new Context(info, base, hierarchy, db_context, classpath, progress)
}
final class Context private[Document_Build](
@@ -132,6 +134,7 @@
base: Sessions.Base,
hierarchy: List[String],
db_context: Sessions.Database_Context,
+ val classpath: List[File.Content_Bytes],
val progress: Progress = new Progress
) {
/* session info */
--- a/src/Pure/Thy/export.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Thy/export.scala Fri Jul 22 16:41:41 2022 +0200
@@ -48,21 +48,52 @@
(if (name == "") "" else " AND " + Data.name.equal(name))
}
- def read_name(
- db: SQL.Database,
- session_name: String,
- theory_name: String,
- name: String
- ): Boolean = {
- val select =
- Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
- db.using_statement(select)(stmt => stmt.execute_query().next())
- }
+ def compound_name(a: String, b: String): String =
+ if (a.isEmpty) b else a + ":" + b
+
+ sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") {
+ val compound_name: String = Export.compound_name(theory, name)
+
+ def make_path(prune: Int = 0): Path = {
+ val elems = theory :: space_explode('/', name)
+ if (elems.length < prune + 1) {
+ error("Cannot prune path by " + prune + " element(s): " + Path.make(elems))
+ }
+ else Path.make(elems.drop(prune))
+ }
+
+ def readable(db: SQL.Database): Boolean = {
+ val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
+ db.using_statement(select)(stmt => stmt.execute_query().next())
+ }
- def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = {
- val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
- db.using_statement(select)(stmt =>
- stmt.execute_query().iterator(res => res.string(Data.name)).toList)
+ def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = {
+ val select =
+ Data.table.select(List(Data.executable, Data.compressed, Data.body),
+ Data.where_equal(session, theory, name))
+ db.using_statement(select) { stmt =>
+ val res = stmt.execute_query()
+ if (res.next()) {
+ val executable = res.bool(Data.executable)
+ val compressed = res.bool(Data.compressed)
+ val bytes = res.bytes(Data.body)
+ val body = Future.value(compressed, bytes)
+ Some(Entry(this, executable, body, cache))
+ }
+ else None
+ }
+ }
+
+ def read(dir: Path, cache: XML.Cache): Option[Entry] = {
+ val path = dir + Path.basic(theory) + Path.explode(name)
+ if (path.is_file) {
+ val executable = File.is_executable(path)
+ val uncompressed = Bytes.read(path)
+ val body = Future.value((false, uncompressed))
+ Some(Entry(this, executable, body, cache))
+ }
+ else None
+ }
}
def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
@@ -72,35 +103,36 @@
stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
}
- def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] = {
+ def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
val select =
Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
" ORDER BY " + Data.theory_name + ", " + Data.name
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
- (res.string(Data.theory_name), res.string(Data.name))).toList)
+ Entry_Name(session = session_name,
+ theory = res.string(Data.theory_name),
+ name = res.string(Data.name))).toList)
}
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
- def compound_name(a: String, b: String): String =
- if (a.isEmpty) b else a + ":" + b
-
def empty_entry(theory_name: String, name: String): Entry =
- Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none)
+ Entry(Entry_Name(theory = theory_name, name = name),
+ false, Future.value(false, Bytes.empty), XML.Cache.none)
sealed case class Entry(
- session_name: String,
- theory_name: String,
- name: String,
+ entry_name: Entry_Name,
executable: Boolean,
body: Future[(Boolean, Bytes)],
cache: XML.Cache
) {
+ def session_name: String = entry_name.session
+ def theory_name: String = entry_name.theory
+ def name: String = entry_name.name
override def toString: String = name
- def compound_name: String = Export.compound_name(theory_name, name)
+ def compound_name: String = entry_name.compound_name
def name_has_prefix(s: String): Boolean = name.startsWith(s)
val name_elems: List[String] = explode_name(name)
@@ -149,13 +181,10 @@
make(Nil, 0, pattern.toList)
}
- def make_matcher(pats: List[String]): (String, String) => Boolean = {
+ def make_matcher(pats: List[String]): Entry_Name => Boolean = {
val regs = pats.map(make_regex)
- {
- (theory_name: String, name: String) =>
- val s = compound_name(theory_name, name)
- regs.exists(_.pattern.matcher(s).matches)
- }
+ (entry_name: Entry_Name) =>
+ regs.exists(_.pattern.matcher(entry_name.compound_name).matches)
}
def make_entry(
@@ -167,47 +196,8 @@
val body =
if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
else Future.value((false, bytes))
- Entry(session_name, args.theory_name, args.name, args.executable, body, cache)
- }
-
- def read_entry(
- db: SQL.Database,
- cache: XML.Cache,
- session_name: String,
- theory_name: String,
- name: String
- ): Option[Entry] = {
- val select =
- Data.table.select(List(Data.executable, Data.compressed, Data.body),
- Data.where_equal(session_name, theory_name, name))
- db.using_statement(select) { stmt =>
- val res = stmt.execute_query()
- if (res.next()) {
- val executable = res.bool(Data.executable)
- val compressed = res.bool(Data.compressed)
- val bytes = res.bytes(Data.body)
- val body = Future.value(compressed, bytes)
- Some(Entry(session_name, theory_name, name, executable, body, cache))
- }
- else None
- }
- }
-
- def read_entry(
- dir: Path,
- cache: XML.Cache,
- session_name: String,
- theory_name: String,
- name: String
- ): Option[Entry] = {
- val path = dir + Path.basic(theory_name) + Path.explode(name)
- if (path.is_file) {
- val executable = File.is_executable(path)
- val uncompressed = Bytes.read(path)
- val body = Future.value((false, uncompressed))
- Some(Entry(session_name, theory_name, name, executable, body, cache))
- }
- else None
+ val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
+ Entry(entry_name, args.executable, body, cache)
}
@@ -232,7 +222,7 @@
entry.body.cancel()
Exn.Res(())
}
- else if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
+ else if (entry.entry_name.readable(db)) {
if (strict) {
val msg = message("Duplicate export", entry.theory_name, entry.name)
errors.change(msg :: _)
@@ -291,7 +281,8 @@
) : Provider = {
new Provider {
def apply(export_name: String): Option[Entry] =
- read_entry(db, cache, session_name, theory_name, export_name)
+ Entry_Name(session = session_name, theory = theory_name, name = export_name)
+ .read(db, cache)
def focus(other_theory: String): Provider =
if (other_theory == theory_name) this
@@ -326,7 +317,8 @@
) : Provider = {
new Provider {
def apply(export_name: String): Option[Entry] =
- read_entry(dir, cache, session_name, theory_name, export_name)
+ Entry_Name(session = session_name, theory = theory_name, name = export_name)
+ .read(dir, cache)
def focus(other_theory: String): Provider =
if (other_theory == theory_name) this
@@ -363,29 +355,21 @@
): Unit = {
using(store.open_database(session_name)) { db =>
db.transaction {
- val export_names = read_theory_exports(db, session_name)
+ val entry_names = read_entry_names(db, session_name)
// list
if (export_list) {
- for ((theory_name, name) <- export_names) {
- progress.echo(compound_name(theory_name, name))
- }
+ for (entry_name <- entry_names) progress.echo(entry_name.compound_name)
}
// export
if (export_patterns.nonEmpty) {
val matcher = make_matcher(export_patterns)
for {
- (theory_name, name) <- export_names if matcher(theory_name, name)
- entry <- read_entry(db, store.cache, session_name, theory_name, name)
+ entry_name <- entry_names if matcher(entry_name)
+ entry <- entry_name.read(db, store.cache)
} {
- val elems = theory_name :: space_explode('/', name)
- val path =
- if (elems.length < export_prune + 1) {
- error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
- }
- else export_dir + Path.make(elems.drop(export_prune))
-
+ val path = export_dir + entry_name.make_path(prune = export_prune)
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
val bytes = entry.uncompressed
--- a/src/Pure/Thy/sessions.ML Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Thy/sessions.ML Fri Jul 22 16:41:41 2022 +0200
@@ -41,6 +41,9 @@
Parse.$$$ "export_files" |--
Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded);
+val export_classpath =
+ Parse.$$$ "export_classpath" |-- Scan.repeat Parse.embedded;
+
fun path_source source path =
Input.source (Input.is_delimited source) (Path.implode path) (Input.range_of source);
@@ -60,10 +63,11 @@
Scan.repeat theories --
Scan.optional document_theories [] --
Scan.repeat document_files --
- Scan.repeat export_files))
+ Scan.repeat export_files --
+ Scan.optional export_classpath []))
>> (fn (((((session, _), _), dir),
- (((((((((parent, descr), options), sessions), directories), theories),
- document_theories), document_files), export_files)))) =>
+ ((((((((((parent, descr), options), sessions), directories), theories),
+ document_theories), document_files), export_files), _)))) =>
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
--- a/src/Pure/Thy/sessions.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Thy/sessions.scala Fri Jul 22 16:41:41 2022 +0200
@@ -429,7 +429,8 @@
theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
document_theories = Nil,
document_files = Nil,
- export_files = Nil))))
+ export_files = Nil,
+ export_classpath = Nil))))
}
}
else (session, Nil)
@@ -466,6 +467,7 @@
document_theories: List[(String, Position.T)],
document_files: List[(Path, Path)],
export_files: List[(Path, Int, List[String])],
+ export_classpath: List[String],
meta_digest: SHA1.Digest
) {
def chapter_session: String = chapter + "/" + name
@@ -599,7 +601,7 @@
Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
entry.parent, entry.description, directories, session_options,
entry.imports, theories, global_theories, entry.document_theories, document_files,
- export_files, meta_digest)
+ export_files, entry.export_classpath, meta_digest)
}
catch {
case ERROR(msg) =>
@@ -860,6 +862,7 @@
private val DOCUMENT_THEORIES = "document_theories"
private val DOCUMENT_FILES = "document_files"
private val EXPORT_FILES = "export_files"
+ private val EXPORT_CLASSPATH = "export_classpath"
val root_syntax: Outer_Syntax =
Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
@@ -873,7 +876,8 @@
(THEORIES, Keyword.QUASI_COMMAND) +
(DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) +
(DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
- (EXPORT_FILES, Keyword.QUASI_COMMAND)
+ (EXPORT_FILES, Keyword.QUASI_COMMAND) +
+ (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
abstract class Entry
sealed case class Chapter(name: String) extends Entry
@@ -890,7 +894,8 @@
theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
document_theories: List[(String, Position.T)],
document_files: List[(String, String)],
- export_files: List[(String, Int, List[String])]
+ export_files: List[(String, Int, List[String])],
+ export_classpath: List[String]
) extends Entry {
def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
@@ -934,6 +939,10 @@
$$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
{ case _ ~ (x ~ y ~ z) => (x, y, z) }
+ val export_classpath =
+ $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^
+ { case _ ~ x => x }
+
command(SESSION) ~!
(position(session_name) ~
(($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
@@ -947,9 +956,10 @@
rep(theories) ~
(opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~
(rep(document_files) ^^ (x => x.flatten)) ~
- rep(export_files)))) ^^
- { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) =>
- Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) }
+ rep(export_files) ~
+ opt(export_classpath)))) ^^
+ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) =>
+ Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) }
}
def parse_root(path: Path): List[Entry] = {
@@ -1216,12 +1226,15 @@
database_server match {
case Some(db) =>
sessions.view.map(session_name =>
- Export.read_entry(db, store.cache, session_name, theory_name, name))
+ Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+ .read(db, store.cache))
case None =>
sessions.view.map(session_name =>
store.try_open_database(session_name) match {
case Some(db) =>
- using(db)(Export.read_entry(_, store.cache, session_name, theory_name, name))
+ using(db) { _ =>
+ Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+ .read(db, store.cache) }
case None => None
})
}
@@ -1233,6 +1246,26 @@
read_export(session_hierarchy, theory_name, name) getOrElse
Export.empty_entry(theory_name, name)
+ def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] =
+ {
+ (for {
+ name <- structure.build_requirements(List(session))
+ patterns = structure(name).export_classpath if patterns.nonEmpty
+ } yield {
+ input_database(name)((db, _) =>
+ db.transaction {
+ val matcher = Export.make_matcher(patterns)
+ val res =
+ for {
+ entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
+ entry <- entry_name.read(db, store.cache)
+ } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
+ Some(res)
+ }
+ ).getOrElse(Nil)
+ }).flatten
+ }
+
override def toString: String = {
val s =
database_server match {
--- a/src/Pure/Tools/generated_files.ML Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Tools/generated_files.ML Fri Jul 22 16:41:41 2022 +0200
@@ -33,6 +33,14 @@
val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
val export_generated_files_cmd: Proof.context ->
((string * Position.T) list * (string * Position.T) option) list -> unit
+ val check_external_files: Proof.context ->
+ Input.source list * Input.source -> Path.T list * Path.T
+ val get_external_files: Path.T -> Path.T list * Path.T -> unit
+ val scala_build_generated_files: Proof.context -> (Path.binding list * theory) list ->
+ (Path.T list * Path.T) list -> unit
+ val scala_build_generated_files_cmd: Proof.context ->
+ ((string * Position.T) list * (string * Position.T) option) list ->
+ (Input.source list * Input.source) list -> unit
val with_compile_dir: (Path.T -> unit) -> unit
val compile_generated_files: Proof.context ->
(Path.binding list * theory) list ->
@@ -272,6 +280,38 @@
export_generated_files ctxt (map (check_files_in ctxt) args);
+(* external files *)
+
+fun check_external_files ctxt (raw_files, raw_base_dir) =
+ let
+ val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
+ fun check source =
+ (Resources.check_file ctxt (SOME base_dir) source;
+ Path.explode (Input.string_of source));
+ val files = map check raw_files;
+ in (files, base_dir) end;
+
+fun get_external_files dir (files, base_dir) =
+ files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir);
+
+
+(* scala_build_generated_files *)
+
+fun scala_build_generated_files ctxt args external =
+ Isabelle_System.with_tmp_dir "scala_build" (fn dir =>
+ let
+ val files = maps get_files_in args;
+ 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);
+
+fun scala_build_generated_files_cmd ctxt args external =
+ scala_build_generated_files ctxt
+ (map (check_files_in ctxt) args)
+ (map (check_external_files ctxt) external)
+
+
(* compile_generated_files *)
val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
@@ -287,9 +327,7 @@
val files = maps get_files_in args;
val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
val _ = List.app (write_file dir o #1) files;
- val _ =
- external |> List.app (fn (files, base_dir) =>
- files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
+ val _ = List.app (get_external_files dir) external;
val _ =
ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
ML_Compiler.flags (Input.pos_of source)
@@ -320,14 +358,7 @@
fun compile_generated_files_cmd ctxt args external export export_prefix source =
compile_generated_files ctxt
(map (check_files_in ctxt) args)
- (external |> map (fn (raw_files, raw_base_dir) =>
- let
- val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
- fun check source =
- (Resources.check_file ctxt (SOME base_dir) source;
- Path.explode (Input.string_of source));
- val files = map check raw_files;
- in (files, base_dir) end))
+ (map (check_external_files ctxt) external)
((map o apfst o map) Path.explode_binding export)
(Path.explode_binding export_prefix)
source;
@@ -352,7 +383,19 @@
(file_type \<^binding>\<open>Haskell\<close>
{ext = "hs",
make_comment = enclose "{-" "-}",
- make_string = GHC.print_string});
+ make_string = GHC.print_string} #>
+ file_type \<^binding>\<open>Java\<close>
+ {ext = "java",
+ make_comment = enclose "/*" "*/",
+ make_string = Java.print_string} #>
+ file_type \<^binding>\<open>Scala\<close>
+ {ext = "scala",
+ make_comment = enclose "/*" "*/",
+ make_string = Java.print_string} #>
+ file_type \<^binding>\<open>Properties\<close>
+ {ext = "props",
+ make_comment = enclose "#" "",
+ make_string = I});
--- a/src/Pure/Tools/scala_build.ML Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Tools/scala_build.ML Fri Jul 22 16:41:41 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 14:21:53 2022 +0000
+++ b/src/Pure/Tools/scala_build.scala Fri Jul 22 16:41:41 2022 +0200
@@ -98,16 +98,14 @@
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
- case None => "result.jar"
+ case None => "scala_build.jar"
}
- List(Bytes("scala_build/" + jar_name), result.jar_bytes, Bytes(result.output))
+ List(Bytes("classpath/" + jar_name), result.jar_bytes, Bytes(result.output))
case _ => error("Bad arguments")
}
}
--- a/src/Pure/Tools/server_commands.scala Fri Jul 22 14:21:53 2022 +0000
+++ b/src/Pure/Tools/server_commands.scala Fri Jul 22 16:41:41 2022 +0200
@@ -264,7 +264,7 @@
("exports" ->
(if (args.export_pattern == "") Nil else {
val matcher = Export.make_matcher(List(args.export_pattern))
- for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
+ for { entry <- snapshot.exports if matcher(entry.entry_name) }
yield {
val (base64, body) = entry.uncompressed.maybe_encode_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)