tuned signature: separate markup vs. extern;

--- 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;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 13:28:01 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 14:41:45 2024 +0200
@@ -703,16 +703,36 @@
 
 local
 
-fun free_or_skolem ctxt x =
+fun markup_fixed ctxt x =
   let
-    val m =
+    val m1 =
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
-  in
-    if Name.is_skolem x
-    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
-    else ([m, Markup.free], x)
-  end;
+    val m2 = if Name.is_skolem x then Markup.skolem else Markup.free;
+  in [m1, m2] end;
+
+fun markup ctxt c =
+  Syntax.get_const (Proof_Context.syntax_of ctxt) c
+  |> Lexicon.unmark
+     {case_class = markup_class ctxt,
+      case_type = markup_type ctxt,
+      case_const = markup_const ctxt,
+      case_fixed = markup_fixed ctxt,
+      case_default = K []};
+
+fun extern_fixed ctxt x =
+  if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
+
+fun extern ctxt c =
+  Syntax.get_const (Proof_Context.syntax_of ctxt) c
+  |> Lexicon.unmark
+     {case_class = Proof_Context.extern_class ctxt,
+      case_type = Proof_Context.extern_type ctxt,
+      case_const = Proof_Context.extern_const ctxt,
+      case_fixed = extern_fixed ctxt,
+      case_default = I};
+
+fun free_or_skolem ctxt x = (markup_fixed ctxt x, extern_fixed ctxt x);
 
 fun var_or_skolem s =
   (case Lexicon.read_variable s of
@@ -725,7 +745,7 @@
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
-fun unparse_t t_to_ast prt_t markup ctxt t =
+fun unparse_t t_to_ast prt_t outer_markup ctxt t =
   let
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
@@ -735,15 +755,6 @@
     val prtabs = Syntax.prtabs syn;
     val trf = Syntax.print_ast_translation syn;
 
-    fun markup_extern c =
-      Syntax.get_const syn c
-      |> Lexicon.unmark
-         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
-          case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
-          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
-          case_fixed = fn x => free_or_skolem ctxt x,
-          case_default = fn x => ([], x)};
-
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
@@ -779,16 +790,16 @@
       else NONE
 
     and pretty_typ_ast m ast = ast
-      |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
+      |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans (markup ctxt, extern ctxt)
       |> Pretty.markup m
 
     and pretty_ast m ast = ast
-      |> prt_t ctxt prtabs trf markup_trans markup_extern
+      |> prt_t ctxt prtabs trf markup_trans (markup ctxt, extern ctxt)
       |> Pretty.markup m;
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
-    |> pretty_ast markup
+    |> pretty_ast outer_markup
   end;
 
 in