src/Pure/Thy/sessions.scala
changeset 74810 d540c36cd0d2
parent 74809 48fda7ee1973
child 74812 4543fb2b5ef2
--- a/src/Pure/Thy/sessions.scala	Wed Nov 17 12:10:48 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 17 12:28:07 2021 +0100
@@ -781,8 +781,7 @@
         else {
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.dir_selected || select_session(name) ||
-              graph.get_node(name).groups.exists(select_group)
+            if info.dir_selected || select_session(name) || info.groups.exists(select_group)
           } yield name).toList
         }