src/Pure/Admin/afp.scala
changeset 66861 f6676691ef8a
parent 66854 e23d73f43fb6
child 67025 961285f581e6
     1.1 --- a/src/Pure/Admin/afp.scala	Sat Oct 14 15:44:21 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Sat Oct 14 16:59:45 2017 +0200
     1.3 @@ -81,4 +81,17 @@
     1.4    }
     1.5   }"""
     1.6      }).mkString("[", ", ", "\n]\n")
     1.7 +
     1.8 +
     1.9 +  /* partition sessions */
    1.10 +
    1.11 +  def partition(n: Int): List[String] =
    1.12 +    n match {
    1.13 +      case 0 => Nil
    1.14 +      case 1 | 2 =>
    1.15 +        val graph = sessions_structure.build_graph.restrict(sessions.toSet)
    1.16 +        val (isolated_sessions, connected_sessions) = graph.keys.partition(graph.is_isolated(_))
    1.17 +        if (n == 1) isolated_sessions else connected_sessions
    1.18 +      case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
    1.19 +    }
    1.20  }