clarified signature: prefer private operation (see also 803731b62180);
authorwenzelm
Fri, 27 Jun 2025 14:52:01 +0200
changeset 82783 98d9abefd9b0
parent 82782 6801c04a7a1a
child 82784 0751d363fd0e
clarified signature: prefer private operation (see also 803731b62180);
src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 27 14:48:37 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Jun 27 14:52:01 2025 +0200
@@ -273,11 +273,6 @@
   def auto_resolve: Boolean = true
   def deps_changed(): Unit = {}
 
-  def commit_change(change: Session.Change): Unit =
-    if (change.deps_changed || auto_resolve && resources.undefined_blobs(change.version).nonEmpty) {
-      deps_changed()
-    }
-
 
   /* buffered changes */
 
@@ -467,7 +462,10 @@
       global_state.change(_.define_version(change.version, assignment))
 
       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
-      commit_change(change)
+
+      if (change.deps_changed || auto_resolve && resources.undefined_blobs(change.version).nonEmpty) {
+        deps_changed()
+      }
     //}}}
     }