# HG changeset patch
# User wenzelm
# Date 1520354659 -3600
# Node ID 44efac3d8638604b8842c2f5eb2e69d3d1d60846
# Parent  8fe8424ff0d3ec40aca2d04718380bf1f5342f85
more balanced AFP partitioning;

diff -r 8fe8424ff0d3 -r 44efac3d8638 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Mar 06 17:43:39 2018 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Mar 06 17:44:19 2018 +0100
@@ -85,12 +85,16 @@
 
   /* partition sessions */
 
+  val force_partition1: List[String] = List("Category3")
+
   def partition(n: Int): List[String] =
     n match {
       case 0 => Nil
       case 1 | 2 =>
         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
-        val (isolated_sessions, connected_sessions) = graph.keys.partition(graph.is_isolated(_))
+        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
       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
     }