--- 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;