# HG changeset patch # User wenzelm # Date 1348919003 -7200 # Node ID 6642e559f165ab77a4583e936abffe7810b0c12e # Parent 366d8b41ca17d379510704efc9b900f4b9bc537a tuned signature; diff -r 366d8b41ca17 -r 6642e559f165 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Sep 28 23:45:15 2012 +0200 +++ b/src/Pure/Syntax/printer.ML Sat Sep 29 13:43:23 2012 +0200 @@ -35,12 +35,12 @@ val merge_prtabs: prtabs -> prtabs -> prtabs val pretty_term_ast: bool -> Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (string -> string -> Pretty.T option) -> + (string -> Ast.ast list -> Pretty.T option) -> (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list val pretty_typ_ast: Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (string -> string -> Pretty.T option) -> + (string -> Ast.ast list -> Pretty.T option) -> (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list end; @@ -167,7 +167,7 @@ val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0))); -fun pretty type_mode curried ctxt tabs trf token_trans markup_extern ast0 = +fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 = let val show_brackets = Config.get ctxt show_brackets; @@ -188,7 +188,7 @@ if type_mode then (astT (t, p) @ Ts, args') else (pretty true curried (Config.put pretty_priority p ctxt) - tabs trf token_trans markup_extern t @ Ts, args') + tabs trf markup_trans markup_extern t @ Ts, args') end | synT m (String s :: symbs, args) = let @@ -242,14 +242,11 @@ astT (appT (splitT n ([c], args)), p) else prnt (prnps, tbs); in - (case tokentrT a args of + (case markup_trans a args of SOME prt => [prt] | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs)) end - and tokentrT a [Ast.Variable x] = token_trans a x - | tokentrT _ _ = NONE - and astT (c as Ast.Constant a, p) = combT (c, a, [], p) | 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) @@ -260,14 +257,14 @@ (* pretty_term_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; +fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast = + pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast; (* pretty_typ_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; +fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast = + pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast; end; diff -r 366d8b41ca17 -r 6642e559f165 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Sep 28 23:45:15 2012 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Sep 29 13:43:23 2012 +0200 @@ -615,6 +615,9 @@ | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x)) | token_trans _ _ = NONE; + fun markup_trans a [Ast.Variable x] = token_trans a x + | markup_trans _ _ = NONE; + fun markup_extern c = (case Syntax.lookup_const syn c of SOME "" => ([], c) @@ -628,7 +631,7 @@ in t_to_ast ctxt (Syntax.print_translation syn) t |> Ast.normalize ctxt (Syntax.print_rules syn) - |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern + |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) markup_trans markup_extern |> Pretty.markup markup end;