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