# HG changeset patch
# User wenzelm
# Date 1666635874 -7200
# Node ID 9bd948666e8ab57b995a1da72912eba6b6b8ee5a
# Parent  b879d2280a7f9e45e65307b217c9279d22825f35
tuned signature, e.g. for Isabelle/DOF;

diff -r b879d2280a7f -r 9bd948666e8a src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Oct 24 15:24:04 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Mon Oct 24 20:24:34 2022 +0200
@@ -124,7 +124,7 @@
   ): Context = new Context(session_context, document_session, progress)
 
   final class Context private[Document_Build](
-    session_context: Export.Session_Context,
+    val session_context: Export.Session_Context,
     document_session: Option[Sessions.Base],
     val progress: Progress = new Progress
   ) {