more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

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