# HG changeset patch
# User haftmann
# Date 1124954593 -7200
# Node ID 5be3a21ec949d46c8040d2038c5afff706393420
# Parent  165c97f9bb63152a9f5807ef06e8e237f26e7a12
added 'default' function

diff -r 165c97f9bb63 -r 5be3a21ec949 src/Pure/General/graph.ML
--- 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
diff -r 165c97f9bb63 -r 5be3a21ec949 src/Pure/General/table.ML
--- 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);