# HG changeset patch
# User wenzelm
# Date 1330172258 -3600
# Node ID 9034b44844bd6edc2aefcccf754dc9660b6c0503
# Parent  318b669fe660b31f4c3ec8b2e49946f05a845ed8
tuned comments;

diff -r 318b669fe660 -r 9034b44844bd src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Feb 25 13:13:14 2012 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 25 13:17:38 2012 +0100
@@ -174,7 +174,7 @@
 fun is_maximal G x = Keys.is_empty (imm_succs G x);
 
 
-(* nodes *)
+(* node operations *)
 
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
@@ -198,7 +198,7 @@
   fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
 
 
-(* edges *)
+(* edge operations *)
 
 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
 
diff -r 318b669fe660 -r 9034b44844bd src/Pure/General/graph.scala
--- 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) }