src/Pure/Syntax/printer.ML

   val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs * prtabs -> prtabs
+  type pretty_ops =
+   {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
+    constrain_output: Ast.ast -> Pretty.T -> Pretty.T,
+    markup_trans: string -> Ast.ast list -> Pretty.T option,
+    markup: string -> Markup.T list,
+    extern: string -> xstring}
   val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list ->
-    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (Ast.ast -> Pretty.T -> Pretty.T) ->
-    (string -> Ast.ast list -> Pretty.T option) ->
-    ((string -> Markup.T list) * (string -> string)) ->
-    Ast.ast -> Pretty.T list
+    pretty_ops -> Ast.ast -> Pretty.T list
   val type_mode_flags: {type_mode: bool, curried: bool}
 end;
 
 structure Printer: PRINTER =
 struct

 
 in
 
 val type_mode_flags = {type_mode = true, curried = false};
 
-fun pretty {type_mode, curried} ctxt prtabs trf constrain_output markup_trans (markup, extern) =
+type pretty_ops =
+ {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
+  constrain_output: Ast.ast -> Pretty.T -> Pretty.T,
+  markup_trans: string -> Ast.ast list -> Pretty.T option,
+  markup: string -> Markup.T list,
+  extern: string -> xstring};
+
+fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) =
   let
     val show_brackets = Config.get ctxt show_brackets;
 
     val application =
       if type_mode then Syntax_Trans.tappl_ast_tr'
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 
     fun constrain_trans (Ast.Appl [Ast.Constant (a as "_constrain"), ast, ty]) =
-          markup_trans a [ast, ty]
+          #markup_trans ops a [ast, ty]
       | constrain_trans _ = NONE;
 
     fun main _ (Ast.Variable x) = [Ast.pretty_var x]
       | main p (cc as Ast.Appl [Ast.Constant "_constrain", c as Ast.Constant a, _]) =
           combination p c a [] (SOME cc)

       | main p (Ast.Appl (f :: (args as _ :: _))) = main p (application (f, args))
       | main _ (ast as Ast.Appl _) = raise Ast.AST ("pretty: malformed ast", [ast])
 
     and main_type p ast =
       if type_mode then main p ast
-      else
-        pretty type_mode_flags (Config.put pretty_priority p ctxt)
-          prtabs trf constrain_output markup_trans (markup, extern) ast
+      else pretty type_mode_flags (Config.put pretty_priority p ctxt) prtabs ops ast
 
     and combination p c a args constraint =
       (case translation p a args of
         SOME prts => prts
       | NONE =>

             (case entry of
               NONE =>
                 if nargs = 0 then
                   (case Option.mapPartial constrain_trans constraint of
                     SOME prt => [prt]
-                  | NONE => [Pretty.marks_str (markup a, extern a)])
+                  | NONE => [Pretty.marks_str (#markup ops a, #extern ops a)])
                 else main p (application (cc, args))
             | SOME (symbs, n, q) =>
                 if nargs = n then parens p q a (symbs, args) constraint
                 else main p (application (split_args n [cc] args)))
           end)
 
     and translation p a args =
-      (case markup_trans a args of
+      (case #markup_trans ops a args of
         SOME prt => SOME [prt]
-      | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE))
+      | NONE => Option.map (main p) (SOME (#trf ops a ctxt args) handle Match => NONE))
 
     and parens p q a (symbs, args) constraint =
       let
         val symbs' =
           if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
           then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
         val output =
           (case constraint of
-            SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => constrain_output ty
+            SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => #constrain_output ops ty
           | _ => I);
-      in #1 (syntax (markup a, output) (symbs', args)) end
+      in #1 (syntax (#markup ops a, output) (symbs', args)) end
 
     and syntax _ ([], args) = ([], args)
       | syntax m (Arg p :: symbs, arg :: args) =
           let val (prts, args') = syntax m (symbs, args);
           in (main p arg @ prts, args') end