tuned messages;
authorwenzelm
Wed, 04 Sep 2019 20:05:57 +0200
changeset 70841 d1d4a1b1ff1f
parent 70840 fa04b549f652
child 70842 d5e4231caa06
tuned messages;
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))