# HG changeset patch
# User haftmann
# Date 1127368576 -7200
# Node ID 78a286d696c1be710cd04baeb3ef072f04594afc
# Parent  830207835ab598c63583fc05b5fdbf1c62812619
added fold_map_graph

diff -r 830207835ab5 -r 78a286d696c1 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Thu Sep 22 07:56:04 2005 +0200
+++ b/src/Pure/General/graph.ML	Thu Sep 22 07:56:16 2005 +0200
@@ -18,6 +18,7 @@
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
+  val fold_map_nodes: (key * 'b -> 'a -> 'c * 'a) -> 'b T -> 'a -> 'c T * 'a
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val imm_preds: 'a T -> key -> key list
@@ -97,6 +98,11 @@
 
 fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
 
+fun fold_map_nodes f (Graph tab) s =
+  s
+  |> Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab
+  |> apfst Graph;
+
 fun get_node G = #1 o get_entry G;
 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));