# HG changeset patch
# User wenzelm
# Date 1660311638 -7200
# Node ID affd69bad2d448eb315ec38f29ac571b1f4f6198
# Parent  d06cae2b407a7101519f72a6cba3626d3e5a79b7
clarified signature: support different document_session, e.g. within running PIDE session;

diff -r d06cae2b407a -r affd69bad2d4 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Aug 12 14:39:37 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Aug 12 15:40:38 2022 +0200
@@ -117,24 +117,27 @@
 
   def context(
     session_context: Export.Session_Context,
+    document_session: Option[Sessions.Base] = None,
     progress: Progress = new Progress
-  ): Context = new Context(session_context, progress)
+  ): Context = new Context(session_context, document_session, progress)
 
   final class Context private[Document_Build](
-    val session_context: Export.Session_Context,
+    session_context: Export.Session_Context,
+    document_session: Option[Sessions.Base],
     val progress: Progress = new Progress
   ) {
     /* session info */
 
-    def session: String = session_context.session_name
+    private val base = document_session getOrElse session_context.session_base
+    private val info = session_context.sessions_structure(base.session_name)
 
-    private val info = session_context.sessions_structure(session)
-    private val base = session_context.session_base
+    def session: String = info.name
+    def options: Options = info.options
+
+    override def toString: String = session
 
     val classpath: List[File.Content_Bytes] = session_context.classpath()
 
-    def options: Options = info.options
-
     def document_bibliography: Boolean = options.bool("document_bibliography")
 
     def document_logo: Option[String] =