# HG changeset patch
# User wenzelm
# Date 1131550008 -3600
# Node ID 1d403623dabc18728380364993af67478cb006b5
# Parent  0e9c9a18f454343982fd0e444ddb8e0c0bb14134
avoid code redundancy;
tuned comments;

diff -r 0e9c9a18f454 -r 1d403623dabc src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Nov 09 16:26:47 2005 +0100
+++ b/src/Pure/General/graph.ML	Wed Nov 09 16:26:48 2005 +0100
@@ -37,7 +37,7 @@
   val add_edge: key * key -> 'a T -> 'a T
   val del_edge: key * key -> 'a T -> 'a T
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
-  val join: (key -> 'a * 'a -> 'a option) -> 'a T * 'a T -> 'a T     (*exception DUPS*)
+  val join: (key -> 'a * 'a -> 'a option) -> 'a T * 'a T -> 'a T      (*exception DUPS*)
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
@@ -114,10 +114,12 @@
   |> apfst Graph;
 
 fun get_node G = #1 o get_entry G;
+
 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
 fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
   let val (a, i') = f i in (a, (i', ps)) end);
 
+
 (* reachability *)
 
 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
@@ -151,6 +153,7 @@
       else tab'
   in Table.empty |> Table.fold subg tab |> Graph end;
 
+
 (* paths *)
 
 fun find_paths G (x, y) =
@@ -204,25 +207,21 @@
 
 (* join and merge *)
 
-fun gen_join add f (Graph tab1, G2 as Graph tab2) =
+fun no_edges (i, _) = (i, ([], []));
+
+fun join f (Graph tab1, G2 as Graph tab2) =
   let
     fun join_node key ((i1, edges1), (i2, _)) =
       (Option.map (rpair edges1) o f key) (i1, i2);
-    fun no_edges (i, _) = (i, ([], []));
-  in fold add (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
-
-(*   val join: (key -> 'a * 'a -> bool) -> 'a T * 'a T -> 'a T           (*exception DUPS*)  *)
-  
-fun join f GG = gen_join add_edge f GG;
+  in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
 
 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
-  let
-    fun eq_node ((i1, _), (i2, _)) = eq (i1, i2);
-    fun no_edges (i, _) = (i, ([], []));
+  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
   in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
 
 fun merge eq GG = gen_merge add_edge eq GG;
 
+
 (* maintain acyclic graphs *)
 
 exception CYCLES of key list list;