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