# HG changeset patch
# User dixon
# Date 1115286960 -7200
# Node ID db77bed00211f5612560ea72955c1afb5a721ee5
# Parent  09fad9a8bc47fe5e8a5652f30218ad4f1e2635b5
lucas - added update node function.

diff -r 09fad9a8bc47 -r db77bed00211 src/Pure/General/graph.ML
--- 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