clarified signature;
authorwenzelm
Fri Mar 23 21:56:22 2018 +0100 (14 months ago)
changeset 6793561888dd27f73
parent 67934 5b0636910618
child 67936 141a93b93aa6
clarified signature;
src/Pure/General/graph.scala
     1.1 --- a/src/Pure/General/graph.scala	Fri Mar 23 20:45:46 2018 +0100
     1.2 +++ b/src/Pure/General/graph.scala	Fri Mar 23 21:56:22 2018 +0100
     1.3 @@ -20,13 +20,14 @@
     1.4    def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     1.5      new Graph[Key, A](SortedMap.empty(ord))
     1.6  
     1.7 -  def make[Key, A](entries: List[((Key, A), List[Key])])(
     1.8 +  def make[Key, A](entries: List[((Key, A), List[Key])], symmetric: Boolean = false)(
     1.9      implicit ord: Ordering[Key]): Graph[Key, A] =
    1.10    {
    1.11      val graph1 =
    1.12        (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    1.13      val graph2 =
    1.14 -      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
    1.15 +      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
    1.16 +        (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
    1.17      graph2
    1.18    }
    1.19