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");
authorwenzelm
Sun Nov 05 16:57:03 2017 +0100 (13 months ago)
changeset 67012671decd2e627
parent 67011 bab3208d8d37
child 67013 335a7dce7cb3
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");
src/Pure/General/graph.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/General/graph.scala	Sun Nov 05 15:50:26 2017 +0100
     1.2 +++ b/src/Pure/General/graph.scala	Sun Nov 05 16:57:03 2017 +0100
     1.3 @@ -70,6 +70,7 @@
     1.4  
     1.5    def keys_iterator: Iterator[Key] = iterator.map(_._1)
     1.6    def keys: List[Key] = keys_iterator.toList
     1.7 +  def keys_set: Set[Key] = rep.keySet
     1.8  
     1.9    def dest: List[((Key, A), List[Key])] =
    1.10      (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
     2.1 --- a/src/Pure/Thy/sessions.scala	Sun Nov 05 15:50:26 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 05 16:57:03 2017 +0100
     2.3 @@ -615,8 +615,8 @@
     2.4  
     2.5      def selection(select: Selection): (List[String], T) =
     2.6      {
     2.7 -      val (_, build_graph1) = select(build_graph)
     2.8        val (selected, imports_graph1) = select(imports_graph)
     2.9 +      val build_graph1 = build_graph.restrict(imports_graph1.keys_set)
    2.10        (selected, new T(build_graph1, imports_graph1))
    2.11      }
    2.12