tuned signature;
authorwenzelm
Tue, 10 Oct 2017 11:24:35 +0200
changeset 66829 5baca4c94737
parent 66828 3c936ebebc23
child 66830 3b50269b90c2
tuned signature;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 10 11:20:02 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 11:24:35 2017 +0200
@@ -355,7 +355,7 @@
   sealed case class Info(
     name: String,
     chapter: String,
-    select: Boolean,
+    dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
@@ -425,7 +425,7 @@
           val select = sessions.toSet ++ graph.all_succs(base_sessions)
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
+            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
       }.filterNot(excluded)