pretty: markup for syntax/name of authentic consts;
authorwenzelm
Sat Jul 07 12:16:18 2007 +0200 (2007-07-07)
changeset 23630bc22daeed49e
parent 23629 8a0cbe8f0566
child 23631 2a9e918653cc
pretty: markup for syntax/name of authentic consts;
datatype symb: String (potential markup) vs. Space (no markup);
src/Pure/Syntax/printer.ML
     1.1 --- a/src/Pure/Syntax/printer.ML	Sat Jul 07 12:16:17 2007 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Sat Jul 07 12:16:18 2007 +0200
     1.3 @@ -31,10 +31,10 @@
     1.4    val merge_prtabs: prtabs -> prtabs -> prtabs
     1.5    val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
     1.6      -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
     1.7 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
     1.8 +    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
     1.9    val pretty_typ_ast: Proof.context -> bool -> prtabs
    1.10      -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    1.11 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
    1.12 +    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
    1.13  end;
    1.14  
    1.15  structure Printer: PRINTER =
    1.16 @@ -188,6 +188,7 @@
    1.17    Arg of int |
    1.18    TypArg of int |
    1.19    String of string |
    1.20 +  Space of string |
    1.21    Break of int |
    1.22    Block of int * symb list;
    1.23  
    1.24 @@ -202,19 +203,16 @@
    1.25  fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
    1.26    | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
    1.27        let
    1.28 -        fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
    1.29 -          | cons_str s syms = String s :: syms;
    1.30 -
    1.31          fun arg (s, p) =
    1.32            (if s = "type" then TypArg else Arg)
    1.33            (if Lexicon.is_terminal s then SynExt.max_pri else p);
    1.34  
    1.35          fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
    1.36 -              apfst (cons_str s) (xsyms_to_syms xsyms)
    1.37 +              apfst (cons (String s)) (xsyms_to_syms xsyms)
    1.38            | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
    1.39                apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
    1.40            | xsyms_to_syms (SynExt.Space s :: xsyms) =
    1.41 -              apfst (cons_str s) (xsyms_to_syms xsyms)
    1.42 +              apfst (cons (Space s)) (xsyms_to_syms xsyms)
    1.43            | xsyms_to_syms (SynExt.Bg i :: xsyms) =
    1.44                let
    1.45                  val (bsyms, xsyms') = xsyms_to_syms xsyms;
    1.46 @@ -230,6 +228,7 @@
    1.47          fun nargs (Arg _ :: syms) = nargs syms + 1
    1.48            | nargs (TypArg _ :: syms) = nargs syms + 1
    1.49            | nargs (String _ :: syms) = nargs syms
    1.50 +          | nargs (Space _ :: syms) = nargs syms
    1.51            | nargs (Break _ :: syms) = nargs syms
    1.52            | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
    1.53            | nargs [] = 0;
    1.54 @@ -267,6 +266,8 @@
    1.55    | is_chain [Arg _] = true
    1.56    | is_chain _  = false;
    1.57  
    1.58 +fun const_markup c = Pretty.markup (Markup.const c) o single;
    1.59 +
    1.60  fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
    1.61    let
    1.62      val trans = apply_trans ctxt "print ast translation";
    1.63 @@ -283,44 +284,47 @@
    1.64        else if curried then SynTrans.applC_ast_tr'
    1.65        else SynTrans.appl_ast_tr';
    1.66  
    1.67 -    fun synT ([], args) = ([], args)
    1.68 -      | synT (Arg p :: symbs, t :: args) =
    1.69 -          let val (Ts, args') = synT (symbs, args);
    1.70 +    fun synT _ ([], args) = ([], args)
    1.71 +      | synT markup (Arg p :: symbs, t :: args) =
    1.72 +          let val (Ts, args') = synT markup (symbs, args);
    1.73            in (astT (t, p) @ Ts, args') end
    1.74 -      | synT (TypArg p :: symbs, t :: args) =
    1.75 +      | synT markup (TypArg p :: symbs, t :: args) =
    1.76            let
    1.77 -            val (Ts, args') = synT (symbs, args);
    1.78 +            val (Ts, args') = synT markup (symbs, args);
    1.79            in
    1.80              if type_mode then (astT (t, p) @ Ts, args')
    1.81              else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
    1.82            end
    1.83 -      | synT (String s :: symbs, args) =
    1.84 -          let val (Ts, args') = synT (symbs, args);
    1.85 +      | synT markup (String s :: symbs, args) =
    1.86 +          let val (Ts, args') = synT markup (symbs, args);
    1.87 +          in (markup (Pretty.str s) :: Ts, args') end
    1.88 +      | synT markup (Space s :: symbs, args) =
    1.89 +          let val (Ts, args') = synT markup (symbs, args);
    1.90            in (Pretty.str s :: Ts, args') end
    1.91 -      | synT (Block (i, bsymbs) :: symbs, args) =
    1.92 +      | synT markup (Block (i, bsymbs) :: symbs, args) =
    1.93            let
    1.94 -            val (bTs, args') = synT (bsymbs, args);
    1.95 -            val (Ts, args'') = synT (symbs, args');
    1.96 +            val (bTs, args') = synT markup (bsymbs, args);
    1.97 +            val (Ts, args'') = synT markup (symbs, args');
    1.98              val T =
    1.99                if i < 0 then Pretty.unbreakable (Pretty.block bTs)
   1.100                else Pretty.blk (i, bTs);
   1.101            in (T :: Ts, args'') end
   1.102 -      | synT (Break i :: symbs, args) =
   1.103 +      | synT markup (Break i :: symbs, args) =
   1.104            let
   1.105 -            val (Ts, args') = synT (symbs, args);
   1.106 +            val (Ts, args') = synT markup (symbs, args);
   1.107              val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
   1.108            in (T :: Ts, args') end
   1.109 -      | synT (_ :: _, []) = sys_error "synT"
   1.110 +      | synT _ (_ :: _, []) = sys_error "synT"
   1.111  
   1.112 -    and parT (pr, args, p, p': int) = #1 (synT
   1.113 +    and parT markup (pr, args, p, p': int) = #1 (synT markup
   1.114            (if p > p' orelse
   1.115              (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
   1.116 -            then [Block (1, String "(" :: pr @ [String ")"])]
   1.117 +            then [Block (1, Space "(" :: pr @ [Space ")"])]
   1.118              else pr, args))
   1.119  
   1.120      and atomT a =
   1.121        (case try (unprefix Lexicon.constN) a of
   1.122 -        SOME c => Pretty.str (extern_const c)
   1.123 +        SOME c => const_markup c (Pretty.str (extern_const c))
   1.124        | NONE =>
   1.125            (case try (unprefix Lexicon.fixedN) a of
   1.126              SOME x =>
   1.127 @@ -340,12 +344,14 @@
   1.128      and combT (tup as (c, a, args, p)) =
   1.129        let
   1.130          val nargs = length args;
   1.131 +        val markup = const_markup (unprefix Lexicon.constN a)
   1.132 +          handle Fail _ => I;
   1.133  
   1.134          (*find matching table entry, or print as prefix / postfix*)
   1.135          fun prnt ([], []) = prefixT tup
   1.136            | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
   1.137            | prnt ((pr, n, p') :: prnps, tbs) =
   1.138 -              if nargs = n then parT (pr, args, p, p')
   1.139 +              if nargs = n then parT markup (pr, args, p, p')
   1.140                else if nargs > n andalso not type_mode then
   1.141                  astT (appT (splitT n ([c], args)), p)
   1.142                else prnt (prnps, tbs);
   1.143 @@ -367,14 +373,14 @@
   1.144  (* pretty_term_ast *)
   1.145  
   1.146  fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
   1.147 -  Pretty.blk (0, pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
   1.148 -    trf tokentrf false curried ast 0);
   1.149 +  pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
   1.150 +    trf tokentrf false curried ast 0;
   1.151  
   1.152  
   1.153  (* pretty_typ_ast *)
   1.154  
   1.155  fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
   1.156 -  Pretty.blk (0, pretty I ctxt (mode_tabs prtabs (! print_mode))
   1.157 -    trf tokentrf true false ast 0);
   1.158 +  pretty I ctxt (mode_tabs prtabs (! print_mode))
   1.159 +    trf tokentrf true false ast 0;
   1.160  
   1.161  end;