# HG changeset patch
# User wenzelm
# Date 1751024676 -7200
# Node ID ec6eb16e4692bb56f1d206a00b4e7f23da35f80d
# Parent  803731b62180ceed1e56c66b0346117aa71b14f6
clarified signature: omit pointless object-oriented indirection;

diff -r 803731b62180 -r ec6eb16e4692 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Fri Jun 27 13:37:36 2025 +0200
+++ b/src/Pure/Build/resources.scala	Fri Jun 27 13:44:36 2025 +0200
@@ -242,17 +242,6 @@
     } yield name).toList
 
 
-  /* document changes */
-
-  def parse_change(
-      reparse_limit: Int,
-      previous: Document.Version,
-      doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text],
-      consolidate: List[Document.Node.Name]): Session.Change =
-    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
-
-
   /* theory and file dependencies */
 
   def dependencies(
diff -r 803731b62180 -r ec6eb16e4692 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 13:37:36 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 27 13:44:36 2025 +0200
@@ -265,7 +265,7 @@
       val prev = previous.get_finished
       val change =
         Timing.timeit(
-          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate),
+          Thy_Syntax.parse_change(resources, reparse_limit, prev, doc_blobs, text_edits, consolidate),
           message = _ => "parse_change",
           enabled = timing)
       version_result.fulfill(change.version)