# HG changeset patch
# User wenzelm
# Date 1214336692 -7200
# Node ID 31f98eaa198d16a117440a4ecafc80902d4dce79
# Parent  b664e5bc95fd8c492f1cd22b8e31b5f4391fe754
pprint: proper output of markup (important for token translation);

diff -r b664e5bc95fd -r 31f98eaa198d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Jun 24 19:43:22 2008 +0200
+++ b/src/Pure/General/pretty.ML	Tue Jun 24 21:44:52 2008 +0200
@@ -322,7 +322,9 @@
 (*ML toplevel pretty printing*)
 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   let
-    fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
+    fun pp (Block (m, prts, ind, _)) =
+          let val (bg, en) = Markup.output m
+          in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
       | pp (String (s, _)) = put_str s
       | pp (Break (false, wd)) = put_brk wd
       | pp (Break (true, _)) = put_fbrk ()