# HG changeset patch # User wenzelm # Date 1510049497 -3600 # Node ID f6aa133f9b16e30260618af9b78490b02ecd8d6f # Parent ce64546693603509d1033eea76d0c36e4871964a backed out odd "bug fix" 671decd2e627; diff -r ce6454669360 -r f6aa133f9b16 src/Pure/General/graph.scala --- 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 diff -r ce6454669360 -r f6aa133f9b16 src/Pure/Thy/sessions.scala --- 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)) }