--- a/src/Pure/General/alist.ML Wed Feb 01 01:05:17 2006 +0100
+++ b/src/Pure/General/alist.ML Wed Feb 01 12:22:19 2006 +0100
@@ -20,6 +20,8 @@
-> ('b * 'c) list -> ('b * 'c) list
val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
-> ('b * 'c) list -> ('b * 'c) list
+ val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c)
+ -> ('b * 'c) list -> 'd option * ('b * 'c) list
val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) ->
('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*)
@@ -73,6 +75,17 @@
| mapp i (x::xs) = x :: mapp (i-1) xs;
in if i = 0 then xs else mapp i xs end;
+fun map_entry_yield eq key f xs =
+ let
+ val i = find_index eq xs key;
+ fun mapp 1 ((x as (key, value))::xs) =
+ let val (r, value') = f value
+ in (SOME r, (key, value') :: xs) end
+ | mapp i (x::xs) =
+ let val (r, xs') = mapp (i-1) xs
+ in (r, x::xs') end;
+ in if i = 0 then (NONE, xs) else mapp i xs end;
+
exception DUP;
fun join eq f (xs, ys) =