# HG changeset patch # User wenzelm # Date 1507800306 -7200 # Node ID 982baed145422c15bd6eb6b3cf7bdf4fa0a4d94b # Parent e8282131ddf97079865d30fcdb42fbd98c4bc939 clarified signature; diff -r e8282131ddf9 -r 982baed14542 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Thu Oct 12 05:37:58 2017 +0200 +++ b/src/Pure/ML/ml_process.scala Thu Oct 12 11:25:06 2017 +0200 @@ -34,7 +34,7 @@ val selection = Sessions.Selection(sessions = List(logic_name)) val (_, selected_sessions) = sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) - (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)). + selected_sessions.build_requirements(List(logic_name)). map(a => File.platform_path(store.heap(a))) } diff -r e8282131ddf9 -r 982baed14542 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Oct 12 05:37:58 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Oct 12 11:25:06 2017 +0200 @@ -509,18 +509,17 @@ (selected, new T(build_graph1, imports_graph1)) } - def build_ancestors(name: String): List[String] = - build_graph.all_preds(List(name)).tail.reverse - def build_descendants(names: List[String]): List[String] = build_graph.all_succs(names) - + def build_requirements(names: List[String]): List[String] = + build_graph.all_preds(names).reverse def build_topological_order: List[Info] = build_graph.topological_order.map(apply(_)) - def imports_ancestors(name: String): List[String] = - imports_graph.all_preds(List(name)).tail.reverse - + def imports_descendants(names: List[String]): List[String] = + imports_graph.all_succs(names) + def imports_requirements(names: List[String]): List[String] = + imports_graph.all_preds(names).reverse def imports_topological_order: List[Info] = imports_graph.topological_order.map(apply(_)) diff -r e8282131ddf9 -r 982baed14542 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Oct 12 05:37:58 2017 +0200 +++ b/src/Pure/Tools/build.scala Thu Oct 12 11:25:06 2017 +0200 @@ -560,7 +560,9 @@ //{{{ check/start next job pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => - val ancestor_results = selected_sessions.build_ancestors(name).map(results(_)) + val ancestor_results = + selected_sessions.build_requirements(List(name)).filterNot(_ == name). + map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp) val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name) diff -r e8282131ddf9 -r 982baed14542 src/Pure/Tools/imports.scala --- a/src/Pure/Tools/imports.scala Thu Oct 12 05:37:58 2017 +0200 +++ b/src/Pure/Tools/imports.scala Thu Oct 12 11:25:06 2017 +0200 @@ -99,8 +99,7 @@ val info = full_sessions(session_name) val session_resources = new Resources(deps(session_name)) - val declared_imports = - full_sessions.imports_ancestors(session_name).toSet + session_name + val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet val extra_imports = (for { (_, a) <- session_resources.session_base.known.theories.iterator