--- a/src/Pure/General/graph.scala Sat Feb 25 13:13:14 2012 +0100
+++ b/src/Pure/General/graph.scala Sat Feb 25 13:17:38 2012 +0100
@@ -119,7 +119,7 @@
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
- /* nodes */
+ /* node operations */
def new_node(x: Key, info: A): Graph[Key, A] =
{
@@ -152,7 +152,7 @@
(this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
- /* edges */
+ /* edge operations */
def is_edge(x: Key, y: Key): Boolean =
try { imm_succs(x)(y) }