--- 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))