src/Pure/Syntax/printer.ML

 datatype symb =
   Arg of int |
   TypArg of int |
   String of bool * string |
   Break of int |
-  Block of {markup: Markup.T, consistent: bool, indent: int} * symb list;
+  Block of Syntax_Ext.block_info * symb list;
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
 fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
 fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);

             val T =
               if do_mark
               then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
               else Pretty.str s;
           in (T :: Ts, args') end
-      | synT m (Block (info, bsymbs) :: symbs, args) =
+      | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
           let
             val (bTs, args') = synT m (bsymbs, args);
             val (Ts, args'') = synT m (symbs, args');
-            val T = Pretty.markup_block info bTs |> #indent info < 0 ? Pretty.unbreakable;
+            val T =
+              Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs
+              |> unbreakable ? Pretty.unbreakable;
           in (T :: Ts, args'') end
       | synT m (Break i :: symbs, args) =
           let
             val (Ts, args') = synT m (symbs, args);
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;