--- 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)
--- 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)