lucas - added update node function.
--- a/src/Pure/General/graph.ML Wed May 04 18:50:39 2005 +0200
+++ b/src/Pure/General/graph.ML Thu May 05 11:56:00 2005 +0200
@@ -27,6 +27,7 @@
val strong_conn: 'a T -> key list list
val find_paths: 'a T -> key * key -> key list list
val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*)
+ val update_node : key * 'a -> 'a T -> 'a T
val del_nodes: key list -> 'a T -> 'a T (*exception UNDEF*)
val is_edge: 'a T -> key * key -> bool
val add_edge: key * key -> 'a T -> 'a T
@@ -145,6 +146,11 @@
fun new_node (x, info) (Graph tab) =
Graph (Table.update_new ((x, (info, ([], []))), tab));
+fun update_node (x, info) (G as Graph tab) =
+ let val (_, (preds, succs)) = get_entry G x in
+ Graph (Table.update ((x, (info, (preds, succs))), tab))
+ end;
+
fun del_nodes xs (Graph tab) =
Graph (tab
|> fold Table.delete xs