# HG changeset patch
# User haftmann
# Date 1127368564 -7200
# Node ID 830207835ab598c63583fc05b5fdbf1c62812619
# Parent  e07af5fad73fd2b438b9e00581283a4997399eb8
added fold_map_table

diff -r e07af5fad73f -r 830207835ab5 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Sep 22 00:30:31 2005 +0200
+++ b/src/Pure/General/table.ML	Thu Sep 22 07:56:04 2005 +0200
@@ -24,6 +24,7 @@
   val map: ('a -> 'b) -> 'a table -> 'b table
   val map': (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+  val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a
   val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
@@ -103,6 +104,25 @@
           fold right (f p2 (fold mid (f p1 (fold left x))));
   in fold end;
 
+fun fold_map_table f = 
+  let
+    fun fold_map Empty s = (Empty, s)
+      | fold_map (Branch2 (left, p as (k, x), right)) s =
+          s
+          |> fold_map left
+          ||>> f p
+          ||>> fold_map right
+          |-> (fn ((l, e), r) => pair (Branch2 (l, (k, e), r)))
+      | fold_map (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) s =
+          s
+          |> fold_map left
+          ||>> f p1
+          ||>> fold_map mid
+          ||>> f p2
+          ||>> fold_map right
+          |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r)))
+  in fold_map end;
+
 fun dest tab = rev (fold_table cons tab []);
 fun keys tab = rev (fold_table (cons o #1) tab []);
 
@@ -363,6 +383,7 @@
 val map' = map_table;
 val fold = fold_table;
 fun foldl f (x, tab) = fold (fn p => fn x' => f (x', p)) tab x;
+val fold_map = fold_map_table;
 
 end;