# HG changeset patch
# User wenzelm
# Date 1751105868 -7200
# Node ID 29d8d6d8a3b14b233c88defa3e0238674a91c301
# Parent  b06207e2215d9e5344e25a58489e3b592df75833
clarified signature;

diff -r b06207e2215d -r 29d8d6d8a3b1 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 15:31:55 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Jun 28 12:17:48 2025 +0200
@@ -270,7 +270,7 @@
       val prev = previous.get_finished
       val change =
         Timing.timeit(
-          Thy_Syntax.parse_change(resources, reparse_limit, prev, doc_blobs, text_edits, consolidate),
+          Thy_Syntax.parse_change(session, reparse_limit, prev, doc_blobs, text_edits, consolidate),
           message = _ => "parse_change",
           enabled = timing)
       version_result.fulfill(change.version)
diff -r b06207e2215d -r 29d8d6d8a3b1 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Jun 27 15:31:55 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 12:17:48 2025 +0200
@@ -294,13 +294,14 @@
   }
 
   def parse_change(
-    resources: Resources,
+    session: Session,
     reparse_limit: Int,
     previous: Document.Version,
     doc_blobs: Document.Blobs,
     edits: List[Document.Edit_Text],
     consolidate: List[Document.Node.Name]
   ): Session.Change = {
+    val resources = session.resources
     val session_base = resources.session_base
 
     val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits)