# HG changeset patch
# User wenzelm
# Date 1751118355 -7200
# Node ID 941b6cdf36117792baf2e2d5190af3554f6cc652
# Parent  5afb8d0d418e251e2651fefe4a6294d3c8344af0
clarified signature;

diff -r 5afb8d0d418e -r 941b6cdf3611 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jun 28 12:27:43 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Jun 28 15:45:55 2025 +0200
@@ -269,8 +269,7 @@
     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
-        Timing.timeit(
-          Thy_Syntax.parse_change(session, reparse_limit, prev, doc_blobs, text_edits, consolidate),
+        Timing.timeit(Thy_Syntax.parse_change(session, prev, doc_blobs, text_edits, consolidate),
           message = _ => "parse_change",
           enabled = timing)
       version_result.fulfill(change.version)
diff -r 5afb8d0d418e -r 941b6cdf3611 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 12:27:43 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 15:45:55 2025 +0200
@@ -295,7 +295,6 @@
 
   def parse_change(
     session: Session,
-    reparse_limit: Int,
     previous: Document.Version,
     doc_blobs: Document.Blobs,
     edits: List[Document.Edit_Text],
@@ -303,6 +302,7 @@
   ): Session.Change = {
     val resources = session.resources
     val session_base = resources.session_base
+    val reparse_limit = session.reparse_limit
 
     val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits)