# HG changeset patch
# User wenzelm
# Date 1509897423 -3600
# Node ID 671decd2e627e97a7278c434aa0d04ce303687cb
# Parent  bab3208d8d37b005f4850502c0f70c6d28555307
uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

diff -r bab3208d8d37 -r 671decd2e627 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sun Nov 05 15:50:26 2017 +0100
+++ b/src/Pure/General/graph.scala	Sun Nov 05 16:57:03 2017 +0100
@@ -70,6 +70,7 @@
 
   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 bab3208d8d37 -r 671decd2e627 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Nov 05 15:50:26 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Nov 05 16:57:03 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))
     }