clarified signature: omit pointless object-oriented indirection;
authorwenzelm
Fri, 27 Jun 2025 13:44:36 +0200
changeset 82779 ec6eb16e4692
parent 82778 803731b62180
child 82780 beba766806ed
clarified signature: omit pointless object-oriented indirection;
src/Pure/Build/resources.scala
src/Pure/PIDE/session.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(
--- 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)