50 let |
50 let |
51 val show_tags = Config.get ctxt show_tags; |
51 val show_tags = Config.get ctxt show_tags; |
52 val show_hyps = Config.get ctxt show_hyps; |
52 val show_hyps = Config.get ctxt show_hyps; |
53 |
53 |
54 val th = Thm.strip_shyps raw_th; |
54 val th = Thm.strip_shyps raw_th; |
55 val {hyps, tpairs, prop, ...} = Thm.rep_thm th; |
55 |
56 val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th; |
56 val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th; |
57 val extra_shyps = Thm.extra_shyps th; |
57 val extra_shyps = Thm.extra_shyps th; |
58 val tags = Thm.get_tags th; |
58 val tags = Thm.get_tags th; |
|
59 val tpairs = Thm.tpairs_of th; |
59 |
60 |
60 val q = if quote then Pretty.quote else I; |
61 val q = if quote then Pretty.quote else I; |
61 val prt_term = q o Syntax.pretty_term ctxt; |
62 val prt_term = q o Syntax.pretty_term ctxt; |
62 |
63 |
63 |
64 |
64 val hlen = length extra_shyps + length hyps' + length tpairs; |
65 val hlen = length extra_shyps + length hyps + length tpairs; |
65 val hsymbs = |
66 val hsymbs = |
66 if hlen = 0 then [] |
67 if hlen = 0 then [] |
67 else if show_hyps orelse show_hyps' then |
68 else if show_hyps orelse show_hyps' then |
68 [Pretty.brk 2, Pretty.list "[" "]" |
69 [Pretty.brk 2, Pretty.list "[" "]" |
69 (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ |
70 (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ |
70 map (Syntax.pretty_sort ctxt) extra_shyps)] |
71 map (Syntax.pretty_sort ctxt) extra_shyps)] |
71 else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
72 else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
72 val tsymbs = |
73 val tsymbs = |
73 if null tags orelse not show_tags then [] |
74 if null tags orelse not show_tags then [] |
74 else [Pretty.brk 1, pretty_tags tags]; |
75 else [Pretty.brk 1, pretty_tags tags]; |
75 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
76 in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; |
76 |
77 |
77 fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
78 fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
78 fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; |
79 fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; |
79 |
80 |
80 fun pretty_thm_global thy = |
81 fun pretty_thm_global thy = |