# HG changeset patch # User wenzelm # Date 1724416905 -7200 # Node ID 94e64d8ac668be03565466f8fcb04964de6d37c9 # Parent 179a24b4020088f24829c0dd98a1dc79427e070d tuned signature: separate markup vs. extern; diff -r 179a24b40200 -r 94e64d8ac668 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; diff -r 179a24b40200 -r 94e64d8ac668 src/Pure/Syntax/syntax_phases.ML --- 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