--- a/src/Pure/General/graph.scala Tue Nov 07 10:22:10 2017 +0100
+++ b/src/Pure/General/graph.scala Tue Nov 07 11:11:37 2017 +0100
@@ -70,7 +70,6 @@
def keys_iterator: Iterator[Key] = iterator.map(_._1)
def keys: List[Key] = keys_iterator.toList
- def keys_set: Set[Key] = rep.keySet
def dest: List[((Key, A), List[Key])] =
(for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
--- a/src/Pure/Thy/sessions.scala Tue Nov 07 10:22:10 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Nov 07 11:11:37 2017 +0100
@@ -615,8 +615,8 @@
def selection(select: Selection): (List[String], T) =
{
+ val (_, build_graph1) = select(build_graph)
val (selected, imports_graph1) = select(imports_graph)
- val build_graph1 = build_graph.restrict(imports_graph1.keys_set)
(selected, new T(build_graph1, imports_graph1))
}