27 |
27 |
28 signature DISPLAY = |
28 signature DISPLAY = |
29 sig |
29 sig |
30 include BASIC_DISPLAY |
30 include BASIC_DISPLAY |
31 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
31 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
32 val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T |
32 val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T |
33 val pretty_thm_no_quote: thm -> Pretty.T |
33 val pretty_thm_no_quote: thm -> Pretty.T |
34 val pretty_thm: thm -> Pretty.T |
34 val pretty_thm: thm -> Pretty.T |
35 val pretty_thms: thm list -> Pretty.T |
35 val pretty_thms: thm list -> Pretty.T |
36 val pretty_thm_sg: theory -> thm -> Pretty.T |
36 val pretty_thm_sg: theory -> thm -> Pretty.T |
37 val pretty_thms_sg: theory -> thm list -> Pretty.T |
37 val pretty_thms_sg: theory -> thm list -> Pretty.T |
64 val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
64 val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
65 |
65 |
66 fun pretty_flexpair pp (t, u) = Pretty.block |
66 fun pretty_flexpair pp (t, u) = Pretty.block |
67 [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; |
67 [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; |
68 |
68 |
69 fun pretty_thm_aux pp quote th = |
69 fun pretty_thm_aux pp quote show_hyps' asms raw_th = |
70 let |
70 let |
|
71 val th = Thm.strip_shyps raw_th; |
71 val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th; |
72 val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th; |
72 val xshyps = Thm.extra_shyps th; |
73 val xshyps = Thm.extra_shyps th; |
73 val (_, tags) = Thm.get_name_tags th; |
74 val (_, tags) = Thm.get_name_tags th; |
74 |
75 |
75 val q = if quote then Pretty.quote else I; |
76 val q = if quote then Pretty.quote else I; |
76 val prt_term = q o (Pretty.term pp); |
77 val prt_term = q o (Pretty.term pp); |
77 |
78 |
78 val hlen = length xshyps + length hyps + length tpairs; |
79 val hyps' = if ! show_hyps then hyps else fold (remove (op =)) asms hyps; |
|
80 val hlen = length xshyps + length hyps' + length tpairs; |
79 val hsymbs = |
81 val hsymbs = |
80 if hlen = 0 andalso not ora then [] |
82 if hlen = 0 andalso not ora then [] |
81 else if ! show_hyps then |
83 else if ! show_hyps orelse show_hyps' then |
82 [Pretty.brk 2, Pretty.list "[" "]" |
84 [Pretty.brk 2, Pretty.list "[" "]" |
83 (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps @ |
85 (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @ |
84 map (Pretty.sort pp) xshyps @ |
86 map (Pretty.sort pp) xshyps @ |
85 (if ora then [Pretty.str "!"] else []))] |
87 (if ora then [Pretty.str "!"] else []))] |
86 else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ |
88 else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ |
87 (if ora then "!" else "") ^ "]")]; |
89 (if ora then "!" else "") ^ "]")]; |
88 val tsymbs = |
90 val tsymbs = |
89 if null tags orelse not (! show_tags) then [] |
91 if null tags orelse not (! show_tags) then [] |
90 else [Pretty.brk 1, pretty_tags tags]; |
92 else [Pretty.brk 1, pretty_tags tags]; |
91 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
93 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
92 |
94 |
93 fun gen_pretty_thm quote th = |
95 fun gen_pretty_thm quote th = |
94 pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote th; |
96 pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote false [] th; |
95 |
97 |
96 val pretty_thm = gen_pretty_thm true; |
98 val pretty_thm = gen_pretty_thm true; |
97 val pretty_thm_no_quote = gen_pretty_thm false; |
99 val pretty_thm_no_quote = gen_pretty_thm false; |
98 |
100 |
99 |
101 |