# HG changeset patch
# User wenzelm
# Date 1567620357 -7200
# Node ID d1d4a1b1ff1f76a4c64504993a8cecc23ae5cd07
# Parent  fa04b549f65273f804184816798390edee2f1e22
tuned messages;

diff -r fa04b549f652 -r d1d4a1b1ff1f src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Wed Sep 04 11:21:07 2019 +0200
+++ b/src/Pure/General/graph.scala	Wed Sep 04 20:05:57 2019 +0200
@@ -14,8 +14,17 @@
 object Graph
 {
   class Duplicate[Key](val key: Key) extends Exception
+  {
+    override def toString: String = "Graph.Duplicate(" + key.toString + ")"
+  }
   class Undefined[Key](val key: Key) extends Exception
+  {
+    override def toString: String = "Graph.Undefined(" + key.toString + ")"
+  }
   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
+  {
+    override def toString: String = cycles.mkString("Graph.Cycles(", ",\n", ")")
+  }
 
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))