proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning "Nothing to build";
--- a/src/Pure/Thy/sessions.scala Wed Oct 12 19:52:03 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Oct 13 11:22:32 2022 +0200
@@ -99,7 +99,7 @@
sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
- def is_empty: Boolean = session_bases.isEmpty
+ def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
def apply(name: String): Base = session_bases(name)
def get(name: String): Option[Base] = session_bases.get(name)