--- 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)