clarified signature;
authorwenzelm
Thu Oct 12 11:25:06 2017 +0200 (19 months ago)
changeset 66848982baed14542
parent 66847 e8282131ddf9
child 66849 42311fd08899
clarified signature;
src/Pure/ML/ml_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Thu Oct 12 05:37:58 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Thu Oct 12 11:25:06 2017 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4          val selection = Sessions.Selection(sessions = List(logic_name))
     1.5          val (_, selected_sessions) =
     1.6            sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
     1.7 -        (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
     1.8 +        selected_sessions.build_requirements(List(logic_name)).
     1.9            map(a => File.platform_path(store.heap(a)))
    1.10        }
    1.11  
     2.1 --- a/src/Pure/Thy/sessions.scala	Thu Oct 12 05:37:58 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Thu Oct 12 11:25:06 2017 +0200
     2.3 @@ -509,18 +509,17 @@
     2.4        (selected, new T(build_graph1, imports_graph1))
     2.5      }
     2.6  
     2.7 -    def build_ancestors(name: String): List[String] =
     2.8 -      build_graph.all_preds(List(name)).tail.reverse
     2.9 -
    2.10      def build_descendants(names: List[String]): List[String] =
    2.11        build_graph.all_succs(names)
    2.12 -
    2.13 +    def build_requirements(names: List[String]): List[String] =
    2.14 +      build_graph.all_preds(names).reverse
    2.15      def build_topological_order: List[Info] =
    2.16        build_graph.topological_order.map(apply(_))
    2.17  
    2.18 -    def imports_ancestors(name: String): List[String] =
    2.19 -      imports_graph.all_preds(List(name)).tail.reverse
    2.20 -
    2.21 +    def imports_descendants(names: List[String]): List[String] =
    2.22 +      imports_graph.all_succs(names)
    2.23 +    def imports_requirements(names: List[String]): List[String] =
    2.24 +      imports_graph.all_preds(names).reverse
    2.25      def imports_topological_order: List[Info] =
    2.26        imports_graph.topological_order.map(apply(_))
    2.27  
     3.1 --- a/src/Pure/Tools/build.scala	Thu Oct 12 05:37:58 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Thu Oct 12 11:25:06 2017 +0200
     3.3 @@ -560,7 +560,9 @@
     3.4              //{{{ check/start next job
     3.5              pending.dequeue(running.isDefinedAt(_)) match {
     3.6                case Some((name, info)) =>
     3.7 -                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
     3.8 +                val ancestor_results =
     3.9 +                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
    3.10 +                    map(results(_))
    3.11                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    3.12  
    3.13                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
     4.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 12 05:37:58 2017 +0200
     4.2 +++ b/src/Pure/Tools/imports.scala	Thu Oct 12 11:25:06 2017 +0200
     4.3 @@ -99,8 +99,7 @@
     4.4          val info = full_sessions(session_name)
     4.5          val session_resources = new Resources(deps(session_name))
     4.6  
     4.7 -        val declared_imports =
     4.8 -          full_sessions.imports_ancestors(session_name).toSet + session_name
     4.9 +        val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet
    4.10          val extra_imports =
    4.11            (for {
    4.12              (_, a) <- session_resources.session_base.known.theories.iterator