src/Pure/General/graph.scala

 
   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
 
 
-  /* nodes */
+  /* node operations */
 
   def new_node(x: Key, info: A): Graph[Key, A] =
   {
     if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)
     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))

 
   def restrict(pred: Key => Boolean): Graph[Key, A] =
     (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) }
     catch { case _: Graph.Undefined[_] => false }