--- a/src/Pure/Thy/document_build.scala Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/document_build.scala Tue Jul 12 15:42:57 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/sessions.ML Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/sessions.ML Tue Jul 12 15:42:57 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 Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Jul 12 15:42:57 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] = {
@@ -1236,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(Path.make(entry.entry_name.elements()), entry.uncompressed)
+ Some(res)
+ }
+ ).getOrElse(Nil)
+ }).flatten
+ }
+
override def toString: String = {
val s =
database_server match {