# HG changeset patch
# User wenzelm
# Date 1521838582 -3600
# Node ID 61888dd27f7380ac0ec0a7e8307bc4f99f43ef4a
# Parent  5b063691061861195126b897b62da1b8a99d3802
clarified signature;

diff -r 5b0636910618 -r 61888dd27f73 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Fri Mar 23 20:45:46 2018 +0100
+++ b/src/Pure/General/graph.scala	Fri Mar 23 21:56:22 2018 +0100
@@ -20,13 +20,14 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])])(
+  def make[Key, A](entries: List[((Key, A), List[Key])], symmetric: Boolean = false)(
     implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
     val graph2 =
-      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
+      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
+        (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
     graph2
   }