# 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