tuned signature;
authorwenzelm
Tue Oct 10 11:24:35 2017 +0200 (19 months ago)
changeset 668295baca4c94737
parent 66828 3c936ebebc23
child 66830 3b50269b90c2
tuned signature;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 10 11:20:02 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 11:24:35 2017 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4    sealed case class Info(
     1.5      name: String,
     1.6      chapter: String,
     1.7 -    select: Boolean,
     1.8 +    dir_selected: Boolean,
     1.9      pos: Position.T,
    1.10      groups: List[String],
    1.11      dir: Path,
    1.12 @@ -425,7 +425,7 @@
    1.13            val select = sessions.toSet ++ graph.all_succs(base_sessions)
    1.14            (for {
    1.15              (name, (info, _)) <- graph.iterator
    1.16 -            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
    1.17 +            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
    1.18            } yield name).toList
    1.19          }
    1.20        }.filterNot(excluded)