# HG changeset patch
# User wenzelm
# Date 1673725368 -3600
# Node ID e5dafe9e120f786e48578de255c255eb1e8efcc8
# Parent  6c542f2aab85d346559d6ba907cdfc485c7eec6b
more robust;

diff -r 6c542f2aab85 -r e5dafe9e120f src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Jan 14 20:15:09 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sat Jan 14 20:42:48 2023 +0100
@@ -56,15 +56,9 @@
     val exclude: Set[String] =
       if (base_logics.isEmpty) Set.empty
       else {
-        val sessions =
-          Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
-            .selection(selection)
-
-        for (name <- base_logics if !sessions.defined(name)) {
-          error("Base logic " + quote(name) + " outside of session selection")
-        }
-
-        sessions.build_requirements(base_logics).toSet
+        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
+          .selection(Sessions.Selection(sessions = base_logics))
+          .build_topological_order.toSet
       }
 
     // test