--- 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 */