src/Pure/General/graph.scala
changeset 67935 61888dd27f73
parent 67018 f6aa133f9b16
child 68321 daca5f2a0c90
equal deleted inserted replaced
67934:5b0636910618 67935:61888dd27f73
    18   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
    18   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
    19 
    19 
    20   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    20   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    21     new Graph[Key, A](SortedMap.empty(ord))
    21     new Graph[Key, A](SortedMap.empty(ord))
    22 
    22 
    23   def make[Key, A](entries: List[((Key, A), List[Key])])(
    23   def make[Key, A](entries: List[((Key, A), List[Key])], symmetric: Boolean = false)(
    24     implicit ord: Ordering[Key]): Graph[Key, A] =
    24     implicit ord: Ordering[Key]): Graph[Key, A] =
    25   {
    25   {
    26     val graph1 =
    26     val graph1 =
    27       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    27       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    28     val graph2 =
    28     val graph2 =
    29       (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
    29       (graph1 /: entries) { case (graph, ((x, _), ys)) =>
       
    30         (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
    30     graph2
    31     graph2
    31   }
    32   }
    32 
    33 
    33   def string[A]: Graph[String, A] = empty(Ordering.String)
    34   def string[A]: Graph[String, A] = empty(Ordering.String)
    34   def int[A]: Graph[Int, A] = empty(Ordering.Int)
    35   def int[A]: Graph[Int, A] = empty(Ordering.Int)