# HG changeset patch
# User wenzelm
# Date 1751028721 -7200
# Node ID 98d9abefd9b046e6cbdfbf481e14d7f2ebab0ca9
# Parent  6801c04a7a1a2dbbc0cd9e4d237b4a6346869a04
clarified signature: prefer private operation (see also 803731b62180);

diff -r 6801c04a7a1a -r 98d9abefd9b0 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()
+      }
     //}}}
     }