# HG changeset patch # User haftmann # Date 1153205291 -7200 # Node ID cf8129ebcdd35d6e636168b9401e004dcd33a003 # Parent 98acc6d0fab6e7e455b90225374d85709092cc0f added Table.map_default diff -r 98acc6d0fab6 -r cf8129ebcdd3 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Tue Jul 18 02:22:38 2006 +0200 +++ b/src/Pure/General/table.ML Tue Jul 18 08:48:11 2006 +0200 @@ -39,6 +39,7 @@ 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 map_default: (key * 'a) -> ('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*) val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> @@ -246,6 +247,7 @@ fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab; fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); +fun map_default (key, x) f = modify key (fn NONE => f x | SOME x => f x); (* delete *)