clarified order --- proper sorting of requirements;

--- 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
 

--- 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(", ",", ")")

--- 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))
         }
 

--- 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 =

--- 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(