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