src/Pure/Syntax/printer.ML

--- a/src/Pure/Syntax/printer.ML	Fri Aug 23 13:28:01 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Aug 23 14:41:45 2024 +0200
@@ -33,12 +33,13 @@
   val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> Ast.ast list -> Pretty.T option) ->
-    (string -> Markup.T list * string) ->
+    ((string -> Markup.T list) * (string -> string)) ->
     Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> Ast.ast list -> Pretty.T option) ->
-    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
+    ((string -> Markup.T list) * (string -> string)) ->
+    Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
@@ -260,7 +261,7 @@
             [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
            else pr, args))
 
-    and atomT a = Pretty.marks_str (markup_extern a)
+    and atomT a = Pretty.marks_str (#1 markup_extern a, #2 markup_extern a)
 
     and prefixT (_, a, [], _) = [atomT a]
       | prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -277,7 +278,7 @@
         fun prnt ([], []) = prefixT tup
           | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
           | prnt ((pr, n, p') :: prnps, tbs) =
-              if nargs = n then parT (#1 (markup_extern a)) (pr, args, p, p')
+              if nargs = n then parT (#1 markup_extern a) (pr, args, p, p')
               else if nargs > n andalso not type_mode then
                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
@@ -297,20 +298,20 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast =
+fun pretty_term_ast curried ctxt prtabs trf markup_trans markup_extern ast =
   let val ctxt' = ctxt
     |> Config.put pretty_type_mode false
     |> Config.put pretty_curried curried
-  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast end;
+  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans markup_extern ast end;
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast =
+fun pretty_typ_ast ctxt prtabs trf markup_trans markup_extern ast =
   let val ctxt' = ctxt
     |> Config.put pretty_type_mode true
     |> Config.put pretty_curried false
-  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast end;
+  in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans markup_extern ast end;
 
 end;