# HG changeset patch
# User wenzelm
# Date 1570977401 -7200
# Node ID 85c2cbd35632d5b8d7836af93862caedfd46926d
# Parent  c92ae7b0f3f1d80c19349e96af8b24640b334209
tuned signature;

diff -r c92ae7b0f3f1 -r 85c2cbd35632 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sun Oct 13 16:26:31 2019 +0200
+++ b/src/Pure/Admin/afp.scala	Sun Oct 13 16:36:41 2019 +0200
@@ -22,6 +22,8 @@
 
   def groups_bulky: List[String] = List("large", "slow")
 
+  val force_partition1: List[String] = List("Category3", "HOL-ODE")
+
   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     new AFP(options, base_dir)
 
@@ -204,15 +206,13 @@
 
   /* partition sessions */
 
-  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_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
+          graph.all_preds(graph.all_succs(AFP.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)")