pretty_sort/typ/term: markup;
authorwenzelm
Sat Jul 07 12:16:19 2007 +0200 (2007-07-07)
changeset 236312a9e918653cc
parent 23630 bc22daeed49e
child 23632 a7df2990f127
pretty_sort/typ/term: markup;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Jul 07 12:16:18 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Jul 07 12:16:19 2007 +0200
     1.3 @@ -511,19 +511,22 @@
     1.4  
     1.5  (** pretty terms, typs, sorts **)
     1.6  
     1.7 -fun pretty_t t_to_ast prt_t ctxt (syn as Syntax (tabs, _)) curried t =
     1.8 +fun pretty_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
     1.9    let
    1.10      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
    1.11      val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
    1.12    in
    1.13 -    prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
    1.14 +    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
    1.15        (lookup_tokentr tokentrtab (! print_mode))
    1.16 -      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
    1.17 +      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
    1.18    end;
    1.19  
    1.20 -val pretty_term = pretty_t Printer.term_to_ast o Printer.pretty_term_ast;
    1.21 -fun pretty_typ ctxt syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast ctxt syn false;
    1.22 -fun pretty_sort ctxt syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast ctxt syn false;
    1.23 +fun pretty_term extern =
    1.24 +  pretty_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
    1.25 +fun pretty_typ ctxt syn =
    1.26 +  pretty_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
    1.27 +fun pretty_sort ctxt syn =
    1.28 +  pretty_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
    1.29  
    1.30  
    1.31