# HG changeset patch
# User wenzelm
# Date 1665652952 -7200
# Node ID 2d4ff8c166d299d3b16e63fe6084567964584d3b
# Parent  6aeb18e8a557857dc36f46a875f0f616dfa5509a
proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning "Nothing to build";

diff -r 6aeb18e8a557 -r 2d4ff8c166d2 src/Pure/Thy/sessions.scala
--- 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)