# HG changeset patch
# User wenzelm
# Date 1330171232 -3600
# Node ID b01b6977a5e862ff70d1da3459f88de413d0c341
# Parent  919dfcdf6d8a90e25886c73f89cf267f2dcb2a14
clarified signature -- avoid oddities of Iterable like Iterator.map;
specific toString;

diff -r 919dfcdf6d8a -r b01b6977a5e8 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sat Feb 25 12:34:56 2012 +0100
+++ b/src/Pure/General/graph.scala	Sat Feb 25 13:00:32 2012 +0100
@@ -24,7 +24,6 @@
 
 
 class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
-  extends Iterable[(Key, (A, (SortedSet[Key], SortedSet[Key])))]
 {
   type Keys = SortedSet[Key]
   type Entry = (A, (Keys, Keys))
@@ -32,17 +31,20 @@
   def ordering: Ordering[Key] = rep.ordering
   def empty_keys: Keys = SortedSet.empty[Key](ordering)
 
-  override def iterator: Iterator[(Key, Entry)] = rep.iterator
+
+  /* graphs */
 
   def is_empty: Boolean = rep.isEmpty
 
-  def keys: List[Key] = rep.keySet.toList
+  def entries: Iterator[(Key, Entry)] = rep.iterator
+  def keys: Iterator[Key] = entries.map(_._1)
 
   def dest: List[(Key, List[Key])] =
-    (for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList
+    (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
 
-
-  /* entries */
+  override def toString: String =
+    dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
+      .mkString("Graph(", ", ", ")")
 
   private def get_entry(x: Key): Entry =
     rep.get(x) match {
@@ -96,7 +98,7 @@
   /*strongly connected components; see: David King and John Launchbury,
     "Structuring Depth First Search Algorithms in Haskell"*/
   def strong_conn: List[List[Key]] =
-    reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
+    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
 
 
   /* minimal and maximal elements */
@@ -143,7 +145,7 @@
   }
 
   def restrict(pred: Key => Boolean): Graph[Key, A] =
-    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+    (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
 
 
   /* edges */