src/Pure/Admin/afp.scala
changeset 67817 93faefc25fe7
parent 67815 8b3d9a91706e
child 69693 06153e2e0cdb
equal deleted inserted replaced
67816:2249b27ab1dd 67817:93faefc25fe7
    83     }).mkString("[", ", ", "\n]\n")
    83     }).mkString("[", ", ", "\n]\n")
    84 
    84 
    85 
    85 
    86   /* partition sessions */
    86   /* partition sessions */
    87 
    87 
    88   val force_partition1: List[String] = List("Category3", "Formula_Derivatives")
    88   val force_partition1: List[String] = List("Category3", "HOL-ODE")
    89 
    89 
    90   def partition(n: Int): List[String] =
    90   def partition(n: Int): List[String] =
    91     n match {
    91     n match {
    92       case 0 => Nil
    92       case 0 => Nil
    93       case 1 | 2 =>
    93       case 1 | 2 =>
    94         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
    94         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
    95         val force_part1 = graph.all_succs(force_partition1.filter(graph.defined(_))).toSet
    95         val force_part1 =
    96         val (isolated_sessions, connected_sessions) =
    96           graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
    97           graph.keys.partition(a => graph.is_isolated(a) || force_part1.contains(a))
    97         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
    98         if (n == 1) isolated_sessions else connected_sessions
    98         if (n == 1) part1 else part2
    99       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
    99       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
   100     }
   100     }
   101 }
   101 }