# HG changeset patch
# User wenzelm
# Date 1742648058 -3600
# Node ID d0838fb98fc3e6c6ddb546cf8f5fa00537f3c152
# Parent  231b6d8231c6a66e0152dcf493bcda073c8fc3e4
clarified signature: more explicit type Sessions.Conditions;

diff -r 231b6d8231c6 -r d0838fb98fc3 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Fri Mar 21 22:26:18 2025 +0100
+++ b/src/Pure/Build/sessions.scala	Sat Mar 22 13:54:18 2025 +0100
@@ -8,7 +8,7 @@
 
 import java.io.{File => JFile}
 
-import scala.collection.immutable.SortedSet
+import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
@@ -552,6 +552,38 @@
     Set.from(notable_groups.flatMap(g => if (g.afp) Some(g.name) else None))
 
 
+  /* conditions to load theories */
+
+  object Conditions {
+    private val empty_rep = SortedMap.empty[String, Boolean]
+    val empty: Conditions = new Conditions(empty_rep)
+    def apply(options: Options): Conditions = make(Set(options))
+    def make(opts: IterableOnce[Options]): Conditions =
+      new Conditions(
+        opts.iterator.flatMap(options => space_explode(',', options.string("condition")).iterator)
+          .foldLeft(empty_rep) {
+            case (map, a) =>
+              if (map.isDefinedAt(a)) map
+              else map + (a -> Isabelle_System.getenv(a).nonEmpty)
+          }
+      )
+  }
+
+  final class Conditions private(private val rep: SortedMap[String, Boolean]) {
+    def toList: List[(String, Boolean)] = rep.toList
+    def good: List[String] = List.from(for ((a, b) <- rep.iterator if b) yield a)
+    def bad: List[String] = List.from(for ((a, b) <- rep.iterator if !b) yield a)
+
+    override def toString: String =
+      if (rep.isEmpty) "Sessions.Conditions.empty"
+      else {
+        val a = if_proper(good, "good = " + quote(good.mkString(",")))
+        val b = if_proper(bad, "bad = " + quote(bad.mkString(",")))
+        "Sessions.Conditions(" + a + if_proper(a.nonEmpty && b.nonEmpty, ", ") + b + ")"
+      }
+  }
+
+
   /* cumulative session info */
 
   private val BUILD_PREFS_BG = "<build_prefs:"
@@ -636,9 +668,7 @@
             else thy_name
           }
 
-        val conditions =
-          theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
-            map(x => (x, Isabelle_System.getenv(x) != ""))
+        val conditions = Conditions.make(theories.iterator.map(_._1)).toList
 
         val document_files =
           entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
diff -r 231b6d8231c6 -r d0838fb98fc3 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Mar 21 22:26:18 2025 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Mar 22 13:54:18 2025 +0100
@@ -237,11 +237,9 @@
           def warn(msg: String): Unit =
             progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
 
-          val conditions =
-            space_explode(',', theory_options.string("condition")).
-              filter(cond => Isabelle_System.getenv(cond) == "")
-          if (conditions.nonEmpty) {
-            warn("undefined " + conditions.mkString(", "))
+          val bad_conditions = Sessions.Conditions(theory_options).bad
+          if (bad_conditions.nonEmpty) {
+            warn("undefined " + bad_conditions.mkString(", "))
             false
           }
           else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) {