--- a/src/Pure/General/graph.scala Wed Jul 25 23:02:50 2012 +0200
+++ b/src/Pure/General/graph.scala Thu Jul 26 11:46:30 2012 +0200
@@ -39,6 +39,7 @@
/* graphs */
def is_empty: Boolean = rep.isEmpty
+ def defined(x: Key): Boolean = rep.isDefinedAt(x)
def entries: Iterator[(Key, Entry)] = rep.iterator
def keys: Iterator[Key] = entries.map(_._1)
@@ -155,8 +156,7 @@
/* edge operations */
def is_edge(x: Key, y: Key): Boolean =
- try { imm_succs(x)(y) }
- catch { case _: Graph.Undefined[_] => false }
+ defined(x) && defined(y) && imm_succs(x)(y)
def add_edge(x: Key, y: Key): Graph[Key, A] =
if (is_edge(x, y)) this