# HG changeset patch
# User wenzelm
# Date 1520770721 -3600
# Node ID 93faefc25fe70cf7cef66cdecdf9957b76be8764
# Parent  2249b27ab1dd1a209be4fe517daa749510d01f42
clarified AFP partitioning;

diff -r 2249b27ab1dd -r 93faefc25fe7 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sat Mar 10 19:36:59 2018 +0000
+++ b/src/Pure/Admin/afp.scala	Sun Mar 11 13:18:41 2018 +0100
@@ -85,17 +85,17 @@
 
   /* partition sessions */
 
-  val force_partition1: List[String] = List("Category3", "Formula_Derivatives")
+  val force_partition1: List[String] = List("Category3", "HOL-ODE")
 
   def partition(n: Int): List[String] =
     n match {
       case 0 => Nil
       case 1 | 2 =>
         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
-        val force_part1 = graph.all_succs(force_partition1.filter(graph.defined(_))).toSet
-        val (isolated_sessions, connected_sessions) =
-          graph.keys.partition(a => graph.is_isolated(a) || force_part1.contains(a))
-        if (n == 1) isolated_sessions else connected_sessions
+        val force_part1 =
+          graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
+        val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
+        if (n == 1) part1 else part2
       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
     }
 }