# HG changeset patch # User wenzelm # Date 1658500901 -7200 # Node ID fc4eaa10ec77ef7fc91e5c436b8a622b5a716155 # Parent acf86c9f769846a503544f425085112bbc54cbe8# Parent 29eb44a65a55a3366e387adc11a9c1d2d56649f7 merged diff -r acf86c9f7698 -r fc4eaa10ec77 src/Doc/Isar_Ref/Spec.thy --- 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>\isabelle-export:\'' (using the regular file-browser). + \<^descr> \<^theory_text>\scala_build_generated_files paths (in thy)\ retrieves named generated + files as for \<^theory_text>\export_generated_files\ 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>\jar\ module becomes an export artifact of the + session database. + \<^descr> \<^theory_text>\compile_generated_files paths (in thy) where compile_body\ retrieves named generated files as for \<^theory_text>\export_generated_files\ and writes them into a temporary directory, such that the \compile_body\ may operate on them as diff -r acf86c9f7698 -r fc4eaa10ec77 src/Doc/System/Scala.thy --- 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>\-q\ suppresses all output on stdout/stderr produced by the Scala or Java compiler. - \<^medskip> Explicit invocation of \<^verbatim>\isabelle scala_build\ 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. \ diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/General/file.scala --- 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)) } diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Pure.thy --- 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>\scala_build_component\ - "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>\scala_build_directory\ - "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>\scala_build_generated_files\ + "build and export Isabelle/Scala/Java module" + (Parse.and_list files_in_theory -- + Scan.optional (\<^keyword>\external_files\ |-- 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\ external_file "ROOT0.ML" diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/ROOT.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"; diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/System/isabelle_system.scala --- 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()) } } } diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/System/java.ML --- /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; diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/System/scala.scala --- 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) } diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Thy/document_build.scala --- 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 */ diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Thy/export.scala --- 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 diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Thy/sessions.ML --- 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; diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Thy/sessions.scala --- 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 { diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Tools/generated_files.ML --- 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>\Haskell\ {ext = "hs", make_comment = enclose "{-" "-}", - make_string = GHC.print_string}); + make_string = GHC.print_string} #> + file_type \<^binding>\Java\ + {ext = "java", + make_comment = enclose "/*" "*/", + make_string = Java.print_string} #> + file_type \<^binding>\Scala\ + {ext = "scala", + make_comment = enclose "/*" "*/", + make_string = Java.print_string} #> + file_type \<^binding>\Properties\ + {ext = "props", + make_comment = enclose "#" "", + make_string = I}); diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Tools/scala_build.ML --- 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>\scala_build\ - [Bytes.string (Value.print_bool component), Bytes.string (Path.implode path)]; + \<^scala>\scala_build\ [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 acf86c9f7698 -r fc4eaa10ec77 src/Pure/Tools/scala_build.scala --- 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") } } diff -r acf86c9f7698 -r fc4eaa10ec77 src/Pure/Tools/server_commands.scala --- 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)