# HG changeset patch
# User wenzelm
# Date 777303405 -7200
# Node ID 6c7e66bcdf489eb5d9a7f2c4bec19c4680e397d0
# Parent  fc92fac8b0deef6333ac56e40e94643b2c58533e
added map_strs: (string -> string) -> T -> T;

diff -r fc92fac8b0de -r 6c7e66bcdf48 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Fri Aug 19 15:36:23 1994 +0200
+++ b/src/Pure/Syntax/pretty.ML	Fri Aug 19 15:36:45 1994 +0200
@@ -45,6 +45,7 @@
   val writeln: T -> unit
   val str_of: T -> string
   val pprint: T -> pprint_args -> unit
+  val map_strs: (string -> string) -> T -> T
   val setdepth: int -> unit
   val setmargin: int -> unit
 end;
@@ -228,6 +229,11 @@
     pp (prune (! depth) prt)
   end;
 
+(*Map strings*)
+fun map_strs f (Block (prts, ind, _)) = blk (ind, map (map_strs f) prts)
+  | map_strs f (String s) = String (f s)
+  | map_strs _ brk = brk;
+
 
 (*** Initialization ***)