src/Pure/Thy/document_build.scala
changeset 75679 aa89255b704c
parent 75394 42267c650205
child 75697 21c1f82e7f5d
--- 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 */