# HG changeset patch
# User haftmann
# Date 1131535265 -3600
# Node ID b74145e46e0d0d1bc75fc3da8b3598529eac9a79
# Parent  50e63c68768fb481ec37cd2629c21bd06af5a6f8
added join function

diff -r 50e63c68768f -r b74145e46e0d src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Nov 08 15:26:35 2005 +0100
+++ b/src/Pure/General/graph.ML	Wed Nov 09 12:21:05 2005 +0100
@@ -37,6 +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*)
   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*)
@@ -201,7 +202,18 @@
 fun edges G = diff_edges G empty;
 
 
-(* merge *)
+(* join and merge *)
+
+fun gen_join add 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;
 
 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   let
@@ -211,7 +223,6 @@
 
 fun merge eq GG = gen_merge add_edge eq GG;
 
-
 (* maintain acyclic graphs *)
 
 exception CYCLES of key list list;