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