# HG changeset patch # User wenzelm # Date 1733580043 -3600 # Node ID 4717d3bf5752eaae57b302faf0b26e22b2c72f77 # Parent a296642fa0a5b03ad17545d3438dbe0039e7f8cd clarified signature and caching; diff -r a296642fa0a5 -r 4717d3bf5752 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Sat Dec 07 11:59:51 2024 +0100 +++ b/src/Pure/Syntax/printer.ML Sat Dec 07 15:00:43 2024 +0100 @@ -39,8 +39,8 @@ constrain_block: Ast.ast -> Markup.output Pretty.block, constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, markup_trans: string -> Ast.ast list -> Pretty.T option, - markup: string -> Markup.T list, - extern: string -> xstring} + markup_syntax: string -> Markup.T list, + pretty_entity: string -> Pretty.T} val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list -> pretty_ops -> Ast.ast -> Pretty.T list val type_mode_flags: {type_mode: bool, curried: bool} @@ -231,8 +231,8 @@ constrain_block: Ast.ast -> Markup.output Pretty.block, constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, markup_trans: string -> Ast.ast list -> Pretty.T option, - markup: string -> Markup.T list, - extern: string -> xstring}; + markup_syntax: string -> Markup.T list, + pretty_entity: string -> Pretty.T}; fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) = let @@ -283,7 +283,7 @@ if nargs = 0 then (case Option.mapPartial constrain_trans constraint of SOME prt => [prt] - | NONE => [Pretty.marks_str (#markup ops a, #extern ops a)]) + | NONE => [#pretty_entity ops a]) else main p (application (cc, args)) | SOME (symbs, n, q) => if nargs = n then parens p q a (symbs, args) constraint @@ -305,7 +305,7 @@ SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => Pretty.make_block (#constrain_block ops ty) o single | _ => I); - in #1 (syntax (#markup ops a, output) (symbs', args)) end + in #1 (syntax (#markup_syntax ops a, output) (symbs', args)) end and syntax _ ([], args) = ([], args) | syntax m (Arg p :: symbs, arg :: args) = diff -r a296642fa0a5 -r 4717d3bf5752 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Dec 07 11:59:51 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Dec 07 15:00:43 2024 +0100 @@ -64,15 +64,14 @@ fun markup_bound def ps (name, id) = Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; -fun markup_entity_cache ctxt = - Symtab.apply_unsynchronized_cache (fn c => - Syntax.get_consts (Proof_Context.syntax_of ctxt) c - |> maps (Lexicon.unmark - {case_class = markup_class ctxt, - case_type = markup_type ctxt, - case_const = markup_const ctxt, - case_fixed = markup_free ctxt, - case_default = K []})); +fun markup_entity ctxt c = + Syntax.get_consts (Proof_Context.syntax_of ctxt) c + |> maps (Lexicon.unmark + {case_class = markup_class ctxt, + case_type = markup_type ctxt, + case_const = markup_const ctxt, + case_fixed = markup_free ctxt, + case_default = K []}); @@ -166,7 +165,7 @@ if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok)) then Position.none else Lexicon.pos_of_token tok; - val markup_cache = markup_entity_cache ctxt; + val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); val ast_of_pos = Ast.Variable o Term_Position.encode; val ast_of_position = ast_of_pos o single o report_pos; @@ -465,7 +464,7 @@ val reports = Unsynchronized.ref ([]: Position.report_text list); fun report ps = Position.store_reports reports ps; - val markup_cache = markup_entity_cache ctxt; + val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); fun decode_const ps c = (report ps markup_cache c; Ast.Constant c); fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x); @@ -712,25 +711,27 @@ local -fun extern_cache ctxt = - Symtab.apply_unsynchronized_cache (fn c => - (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of - [b] => b - | bs => - (case filter Lexicon.is_marked bs of - [] => c - | [b] => b - | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) - |> Proof_Context.extern_entity ctxt); +fun extern ctxt c = + (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of + [b] => b + | bs => + (case filter Lexicon.is_marked bs of + [] => c + | [b] => b + | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) + |> Proof_Context.extern_entity ctxt; -val var_or_skolem_cache = - Symtab.apply_unsynchronized_cache (fn s => - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - SOME x' => (Markup.skolem, Term.string_of_vname (x', i)) - | NONE => (Markup.var, s)) - | NONE => (Markup.var, s))); +fun pretty_free ctxt x = + Pretty.marks_str (markup_free ctxt x, Proof_Context.extern_fixed ctxt x); + +fun pretty_var s = + (case Lexicon.read_variable s of + SOME (x, i) => + (case try Name.dest_skolem x of + SOME x' => (Markup.skolem, Term.string_of_vname (x', i)) + | NONE => (Markup.var, s)) + | NONE => (Markup.var, s)) + |> Pretty.mark_str; val typing_elem = YXML.output_markup_elem Markup.typing; val sorting_elem = YXML.output_markup_elem Markup.sorting; @@ -761,22 +762,24 @@ val show_sorts = Config.get ctxt show_sorts; val show_types = Config.get ctxt show_types orelse show_sorts; - val markup = markup_entity_cache ctxt; - val extern = extern_cache ctxt; + val pretty_free_cache = Symtab.apply_unsynchronized_cache (pretty_free ctxt); + val pretty_var_cache = Symtab.apply_unsynchronized_cache pretty_var; - val free_or_skolem_cache = - Symtab.apply_unsynchronized_cache (fn x => - (markup_free ctxt x, Proof_Context.extern_fixed ctxt x)); + val markup_syntax_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); + + val pretty_entity_cache = + Symtab.apply_unsynchronized_cache (fn a => + Pretty.marks_str (markup_syntax_cache a, extern ctxt a)); val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); 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_cache x)) + | token_trans "_free" x = SOME (pretty_free_cache x) | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x)) - | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem_cache x)) + | token_trans "_var" x = SOME (pretty_var_cache x) | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) | token_trans _ _ = NONE; @@ -798,7 +801,8 @@ and pretty_ast flags m = Printer.pretty flags ctxt prtabs {trf = trf, constrain_block = constrain_block true, constrain_trans = constrain_trans, - markup_trans = markup_trans, markup = markup, extern = extern} + markup_trans = markup_trans, markup_syntax = markup_syntax_cache, + pretty_entity = pretty_entity_cache} #> Pretty.markup m and markup_ast is_typing a A =