# HG changeset patch
# User haftmann
# Date 1138792939 -3600
# Node ID 1bbeb076a6dec868961f48a967e05c345dc91c11
# Parent  454d09651d1a82cc2f47128d52a6bc8ea3534abd
added map_entry_yield

diff -r 454d09651d1a -r 1bbeb076a6de src/Pure/General/alist.ML
--- 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) =