--- a/src/Pure/General/graph.ML Wed Aug 24 12:07:00 2005 +0200
+++ b/src/Pure/General/graph.ML Thu Aug 25 09:23:13 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 default_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
@@ -143,6 +144,9 @@
fun new_node (x, info) (Graph tab) =
Graph (Table.update_new ((x, (info, ([], []))), tab));
+fun default_node x info (Graph tab) =
+ Graph (Table.default x (info, ([], [])) tab);
+
fun del_nodes xs (Graph tab) =
Graph (tab
|> fold Table.delete xs
--- a/src/Pure/General/table.ML Wed Aug 24 12:07:00 2005 +0200
+++ b/src/Pure/General/table.ML Thu Aug 25 09:23:13 2005 +0200
@@ -35,6 +35,7 @@
val lookup: 'a table * key -> 'a option
val update: (key * 'a) * 'a table -> 'a table
val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*)
+ val default: key -> 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUPS*)
val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*)
@@ -203,6 +204,7 @@
fun update ((key, x), tab) = modify key (fn _ => x) tab;
fun update_new ((key, x), tab) = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
+fun default key x tab = if defined tab key then tab else update ((key, x), tab)
fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);