# HG changeset patch # User wenzelm # Date 1595507148 -7200 # Node ID 11dc8929832d23bd15770456d8735e191ffc72ad # Parent ce844442e2abce4d7a4faf644243acc5da50c485 clarified order --- proper sorting of requirements; diff -r ce844442e2ab -r 11dc8929832d src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Thu Jul 23 11:48:58 2020 +0200 +++ b/src/Pure/General/graph.scala Thu Jul 23 14:25:48 2020 +0200 @@ -154,14 +154,16 @@ } /*reachable nodes with result in topological order (for acyclic graphs)*/ - def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = + private def reachable(next: Key => Keys, xs: List[Key], rev: Boolean = false): (List[List[Key]], Keys) = { def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) = { val (rs, r_set) = reached if (r_set(x)) reached else { - val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach) + val (rs1, r_set1) = + if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) }) + else (next(x) :\ (rs, r_set + x))(reach) (x :: rs1, r_set1) } } @@ -179,6 +181,8 @@ def imm_succs(x: Key): Keys = get_entry(x)._2._2 /*transitive*/ + def all_preds_rev(xs: List[Key]): List[Key] = + reachable(imm_preds, xs, rev = true)._1.flatten.reverse def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten diff -r ce844442e2ab -r 11dc8929832d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Jul 23 11:48:58 2020 +0200 +++ b/src/Pure/PIDE/document.scala Thu Jul 23 14:25:48 2020 +0200 @@ -408,7 +408,7 @@ } yield cmd).toList def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) - def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse + def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names) def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")") diff -r ce844442e2ab -r 11dc8929832d src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Thu Jul 23 11:48:58 2020 +0200 +++ b/src/Pure/PIDE/headless.scala Thu Jul 23 14:25:48 2020 +0200 @@ -105,7 +105,7 @@ def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) : (List[Document.Node.Name], Load_State) = { - val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished) + val load_theories = dep_graph.all_preds_rev(pending1).filterNot(finished) (load_theories, Load_State(pending1, rest1, load_limit)) } diff -r ce844442e2ab -r 11dc8929832d src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Jul 23 11:48:58 2020 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Jul 23 14:25:48 2020 +0200 @@ -715,12 +715,12 @@ def build_selection(sel: Selection): List[String] = selected(build_graph, sel) def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) - def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse + def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) def build_topological_order: List[String] = build_graph.topological_order def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel) def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss) - def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse + def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order override def toString: String = diff -r ce844442e2ab -r 11dc8929832d src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Jul 23 11:48:58 2020 +0200 +++ b/src/Pure/Tools/dump.scala Thu Jul 23 14:25:48 2020 +0200 @@ -169,7 +169,7 @@ (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList val base_sessions = - session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse + session_graph.all_preds_rev(List(logic).filter(session_graph.defined)) val proof_sessions = session_graph.all_succs(