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