# HG changeset patch
# User wenzelm
# Date 1675623914 -3600
# Node ID 9b35c1171d9ac9c76cd97eb168c2cbe7e167dd31
# Parent  a541da01ba67e8f113130b670cda19b9c08cba64
more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

diff -r a541da01ba67 -r 9b35c1171d9a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Feb 05 15:59:18 2023 +0100
+++ b/src/Pure/PIDE/session.scala	Sun Feb 05 20:05:14 2023 +0100
@@ -618,10 +618,11 @@
                 case None => consolidation.update()
                 case Some(version) =>
                   val consolidate =
-                    consolidation.flush().iterator.filter(name =>
+                    version.nodes.descendants(consolidation.flush().toList).filter { name =>
                       !resources.session_base.loaded_theory(name) &&
                       !state.node_consolidated(version, name) &&
-                      state.node_maybe_consolidated(version, name)).toList
+                      state.node_maybe_consolidated(version, name)
+                    }
                   if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
               }
             }