# HG changeset patch # User wenzelm # Date 1302191564 -7200 # Node ID 9566078ad9057eb97feb7724a5c62a9d64927828 # Parent f87e0be80a3f9a59368b559228d1c4e4f01d788a simplified printer context: uniform externing and static token translations; diff -r f87e0be80a3f -r 9566078ad905 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 07 17:38:17 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 07 17:52:44 2011 +0200 @@ -400,40 +400,6 @@ | NONE => x); -(* default token translations *) - -local - -fun free_or_skolem ctxt x = - (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x)) - else Pretty.mark Markup.free (Pretty.str x)) - |> Pretty.mark - (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x - else Markup.hilite); - -fun var_or_skolem _ s = - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - NONE => Pretty.mark Markup.var (Pretty.str s) - | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i)))) - | NONE => Pretty.mark Markup.var (Pretty.str s)); - -fun plain_markup m _ s = Pretty.mark m (Pretty.str s); - -val token_trans = - Syntax.tokentrans_mode "" - [("tfree", plain_markup Markup.tfree), - ("tvar", plain_markup Markup.tvar), - ("free", free_or_skolem), - ("bound", plain_markup Markup.bound), - ("var", var_or_skolem), - ("numeral", plain_markup Markup.numeral), - ("inner_string", plain_markup Markup.inner_string)]; - -in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end; - - (** prepare terms and propositions **) diff -r f87e0be80a3f -r 9566078ad905 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Apr 07 17:38:17 2011 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Apr 07 17:52:44 2011 +0200 @@ -33,14 +33,15 @@ val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs val merge_prtabs: prtabs -> prtabs -> prtabs - val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring, - extern_const: string -> xstring} -> Proof.context -> bool -> prtabs -> + val pretty_term_ast: bool -> Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list - val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} -> - Proof.context -> bool -> prtabs -> + (string -> string -> Pretty.T option) -> + (string -> Markup.T list * xstring) -> + Ast.ast -> Pretty.T list + val pretty_typ_ast: Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list + (string -> string -> Pretty.T option) -> + (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list end; structure Printer: PRINTER = @@ -166,18 +167,10 @@ val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0))); -fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 = +fun pretty type_mode curried ctxt tabs trf token_trans markup_extern ast0 = let - val {extern_class, extern_type, extern_const} = extern; val show_brackets = Config.get ctxt show_brackets; - fun token_trans a x = - (case tokentrf a of - NONE => - if member (op =) Syn_Ext.standard_token_classes a - then SOME (Pretty.str x) else NONE - | SOME f => SOME (f ctxt x)); - (*default applications: prefix / postfix*) val appT = if type_mode then Syn_Trans.tappl_ast_tr' @@ -185,49 +178,44 @@ else Syn_Trans.appl_ast_tr'; fun synT _ ([], args) = ([], args) - | synT markup (Arg p :: symbs, t :: args) = - let val (Ts, args') = synT markup (symbs, args); + | synT m (Arg p :: symbs, t :: args) = + let val (Ts, args') = synT m (symbs, args); in (astT (t, p) @ Ts, args') end - | synT markup (TypArg p :: symbs, t :: args) = + | synT m (TypArg p :: symbs, t :: args) = let - val (Ts, args') = synT markup (symbs, args); + val (Ts, args') = synT m (symbs, args); in if type_mode then (astT (t, p) @ Ts, args') else - (pretty extern (Config.put pretty_priority p ctxt) - tabs trf tokentrf true curried t @ Ts, args') + (pretty true curried (Config.put pretty_priority p ctxt) + tabs trf token_trans markup_extern t @ Ts, args') end - | synT markup (String s :: symbs, args) = - let val (Ts, args') = synT markup (symbs, args); - in (markup (Pretty.str s) :: Ts, args') end - | synT markup (Space s :: symbs, args) = - let val (Ts, args') = synT markup (symbs, args); + | synT m (String s :: symbs, args) = + let val (Ts, args') = synT m (symbs, args); + in (Pretty.marks_str (m, s) :: Ts, args') end + | synT m (Space s :: symbs, args) = + let val (Ts, args') = synT m (symbs, args); in (Pretty.str s :: Ts, args') end - | synT markup (Block (i, bsymbs) :: symbs, args) = + | synT m (Block (i, bsymbs) :: symbs, args) = let - val (bTs, args') = synT markup (bsymbs, args); - val (Ts, args'') = synT markup (symbs, args'); + val (bTs, args') = synT m (bsymbs, args); + val (Ts, args'') = synT m (symbs, args'); val T = if i < 0 then Pretty.unbreakable (Pretty.block bTs) else Pretty.blk (i, bTs); in (T :: Ts, args'') end - | synT markup (Break i :: symbs, args) = + | synT m (Break i :: symbs, args) = let - val (Ts, args') = synT markup (symbs, args); + val (Ts, args') = synT m (symbs, args); val T = if i < 0 then Pretty.fbrk else Pretty.brk i; in (T :: Ts, args') end - and parT markup (pr, args, p, p': int) = #1 (synT markup + and parT m (pr, args, p, p': int) = #1 (synT m (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr)) then [Block (1, Space "(" :: pr @ [Space ")"])] else pr, args)) - and atomT a = a |> Lexicon.unmark - {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)), - case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)), - case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)), - case_fixed = fn x => the (token_trans "_free" x), - case_default = Pretty.str} + and atomT a = Pretty.marks_str (markup_extern a) and prefixT (_, a, [], _) = [atomT a] | prefixT (c, _, args, p) = astT (appT (c, args), p) @@ -239,18 +227,12 @@ and combT (tup as (c, a, args, p)) = let val nargs = length args; - val markup = a |> Lexicon.unmark - {case_class = Pretty.mark o Markup.tclass, - case_type = Pretty.mark o Markup.tycon, - case_const = Pretty.mark o Markup.const, - case_fixed = Pretty.mark o Markup.fixed, - case_default = K I}; (*find matching table entry, or print as prefix / postfix*) 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 markup (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); @@ -264,7 +246,7 @@ | tokentrT _ _ = NONE and astT (c as Ast.Constant a, p) = combT (c, a, [], p) - | astT (ast as Ast.Variable x, _) = [Ast.pretty_ast ast] + | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast] | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p) | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]); @@ -273,14 +255,13 @@ (* pretty_term_ast *) -fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast = - pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf false curried ast; +fun pretty_term_ast curried ctxt prtabs trf tokentrf extern ast = + pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast; (* pretty_typ_ast *) -fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast = - pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I} - ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf true false ast; +fun pretty_typ_ast ctxt prtabs trf tokentrf extern ast = + pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast; end; diff -r f87e0be80a3f -r 9566078ad905 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Apr 07 17:38:17 2011 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Thu Apr 07 17:52:44 2011 +0200 @@ -15,11 +15,7 @@ val mk_trfun: string * 'a -> string * ('a * stamp) val eq_trfun: ('a * stamp) * ('a * stamp) -> bool val escape: string -> string - val tokentrans_mode: - string -> (string * (Proof.context -> string -> Pretty.T)) list -> - (string * string * (Proof.context -> string -> Pretty.T)) list - val standard_token_classes: string list - val standard_token_markers: string list + val token_markers: string list end; signature SYN_EXT = @@ -383,17 +379,10 @@ fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; -(* token translations *) - -fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; +(* pure_ext *) -val standard_token_classes = - ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"]; - -val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes; - - -(* pure_ext *) +val token_markers = + ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; val pure_ext = syn_ext' false (K false) [Mfix ("_", spropT --> propT, "", [0], 0), @@ -403,7 +392,7 @@ Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] - standard_token_markers + token_markers ([], [], [], []) [] ([], []); diff -r f87e0be80a3f -r 9566078ad905 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Apr 07 17:38:17 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Apr 07 17:52:44 2011 +0200 @@ -475,7 +475,7 @@ val {structs, fixes} = idents; fun mark_atoms ((t as Const (c, _)) $ u) = - if member (op =) Syntax.standard_token_markers c + if member (op =) Syntax.token_markers c then t $ u else mark_atoms t $ mark_atoms u | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) @@ -553,46 +553,66 @@ local -fun unparse_t t_to_ast prt_t markup ctxt curried t = +fun free_or_skolem ctxt x = + let + val m = + if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt + then Markup.fixed x + else Markup.hilite; + in + if can Name.dest_skolem x + then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x) + else ([m, Markup.free], x) + end; + +fun var_or_skolem s = + (case Lexicon.read_variable s of + SOME (x, i) => + (case try Name.dest_skolem x of + NONE => (Markup.var, s) + | SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) + | NONE => (Markup.var, s)); + +fun unparse_t t_to_ast prt_t markup ctxt t = let val syn = ProofContext.syn_of ctxt; - val tokentr = Syntax.token_translation syn (print_mode_value ()); + + 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)) + | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) + | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem 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; + + val markup_extern = Lexicon.unmark + {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x), + case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x), + case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x), + case_fixed = fn x => free_or_skolem ctxt x, + case_default = fn x => ([], x)}; in t_to_ast ctxt (Syntax.print_translation syn) t |> Ast.normalize ctxt (Syntax.print_rules syn) - |> prt_t ctxt curried (Syntax.prtabs syn) (Syntax.print_ast_translation syn) tokentr + |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern |> Pretty.markup markup end; in -fun unparse_sort ctxt = - let - val tsig = ProofContext.tsig_of ctxt; - val extern = {extern_class = Type.extern_class tsig, extern_type = I}; - in unparse_t sort_to_ast (Printer.pretty_typ_ast extern) Markup.sort ctxt false end; - -fun unparse_typ ctxt = - let - val tsig = ProofContext.tsig_of ctxt; - val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; - in unparse_t typ_to_ast (Printer.pretty_typ_ast extern) Markup.typ ctxt false end; +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort; +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ; fun unparse_term ctxt = let val thy = ProofContext.theory_of ctxt; val syn = ProofContext.syn_of ctxt; - val tsig = ProofContext.tsig_of ctxt; val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt); - val is_syntax_const = Syntax.is_const syn; - val consts = ProofContext.consts_of ctxt; - val extern = - {extern_class = Type.extern_class tsig, - extern_type = Type.extern_type tsig, - extern_const = Consts.extern consts}; in - unparse_t (term_to_ast idents is_syntax_const) (Printer.pretty_term_ast extern) - Markup.term ctxt (not (Pure_Thy.old_appl_syntax thy)) + unparse_t (term_to_ast idents (Syntax.is_const syn)) + (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) + Markup.term ctxt end; end;