# HG changeset patch
# User haftmann
# Date 1131977707 -3600
# Node ID 4f9410e685df767b0e125a07ef68319f8b9d370b
# Parent  b7c3136f604dc9268172e99689e931f7bf7060a9
string_of_alist - convenient q'n'd  printout function

diff -r b7c3136f604d -r 4f9410e685df src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Mon Nov 14 15:14:59 2005 +0100
+++ b/src/Pure/General/alist.ML	Mon Nov 14 15:15:07 2005 +0100
@@ -26,6 +26,7 @@
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
     -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
+  val string_of_alist: ('a -> string) -> ('b -> string) -> ('a * 'b) list -> string
 end;
 
 structure AList: ALIST =
@@ -107,4 +108,9 @@
         val values = find eq xs value';
       in if eq (value', value) then key :: values else values end;
 
+fun string_of_alist string_of_key string_of_value =
+  map (fn (key, value) => string_of_key key ^ " -> " ^ string_of_value value)
+  #> commas
+  #> enclose "[" "]"
+
 end;