16 end; |
16 end; |
17 |
17 |
18 signature DISPLAY = |
18 signature DISPLAY = |
19 sig |
19 sig |
20 include BASIC_DISPLAY |
20 include BASIC_DISPLAY |
21 val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} -> |
21 val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T |
22 thm -> Pretty.T |
|
23 val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T |
|
24 val pretty_thm: Proof.context -> thm -> Pretty.T |
22 val pretty_thm: Proof.context -> thm -> Pretty.T |
25 val pretty_thm_global: theory -> thm -> Pretty.T |
23 val pretty_thm_global: theory -> thm -> Pretty.T |
26 val pretty_thm_without_context: thm -> Pretty.T |
24 val pretty_thm_without_context: thm -> Pretty.T |
27 val string_of_thm: Proof.context -> thm -> string |
25 val string_of_thm: Proof.context -> thm -> string |
28 val string_of_thm_global: theory -> thm -> string |
26 val string_of_thm_global: theory -> thm -> string |
29 val string_of_thm_without_context: thm -> string |
27 val string_of_thm_without_context: thm -> string |
30 val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T |
|
31 val pretty_thms: Proof.context -> thm list -> Pretty.T |
28 val pretty_thms: Proof.context -> thm list -> Pretty.T |
32 val print_syntax: theory -> unit |
29 val print_syntax: theory -> unit |
33 val pretty_full_theory: bool -> theory -> Pretty.T list |
30 val pretty_full_theory: bool -> theory -> Pretty.T list |
34 end; |
31 end; |
35 |
32 |
52 (** print thm **) |
49 (** print thm **) |
53 |
50 |
54 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; |
51 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; |
55 val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
52 val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
56 |
53 |
57 fun display_status _ false _ = "" |
54 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = |
58 | display_status show_hyps true th = |
|
59 let |
|
60 val {oracle = oracle0, unfinished, failed} = Thm.status_of th; |
|
61 val oracle = oracle0 andalso (not (! quick_and_dirty) orelse show_hyps); |
|
62 in |
|
63 if failed then "!!" |
|
64 else if oracle andalso unfinished then "!?" |
|
65 else if oracle then "!" |
|
66 else if unfinished then "?" |
|
67 else "" |
|
68 end; |
|
69 |
|
70 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th = |
|
71 let |
55 let |
72 val show_tags = Config.get ctxt show_tags; |
56 val show_tags = Config.get ctxt show_tags; |
73 val show_hyps = Config.get ctxt show_hyps; |
57 val show_hyps = Config.get ctxt show_hyps; |
74 |
58 |
75 val th = Thm.strip_shyps raw_th; |
59 val th = Thm.strip_shyps raw_th; |
80 val q = if quote then Pretty.quote else I; |
64 val q = if quote then Pretty.quote else I; |
81 val prt_term = q o Syntax.pretty_term ctxt; |
65 val prt_term = q o Syntax.pretty_term ctxt; |
82 |
66 |
83 val asms = map Thm.term_of (Assumption.all_assms_of ctxt); |
67 val asms = map Thm.term_of (Assumption.all_assms_of ctxt); |
84 val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps; |
68 val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps; |
85 val status = display_status show_hyps show_status th; |
|
86 |
69 |
87 val hlen = length xshyps + length hyps' + length tpairs; |
70 val hlen = length xshyps + length hyps' + length tpairs; |
88 val hsymbs = |
71 val hsymbs = |
89 if hlen = 0 andalso status = "" then [] |
72 if hlen = 0 then [] |
90 else if show_hyps orelse show_hyps' then |
73 else if show_hyps orelse show_hyps' then |
91 [Pretty.brk 2, Pretty.list "[" "]" |
74 [Pretty.brk 2, Pretty.list "[" "]" |
92 (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ |
75 (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ |
93 map (Syntax.pretty_sort ctxt) xshyps @ |
76 map (Syntax.pretty_sort ctxt) xshyps)] |
94 (if status = "" then [] else [Pretty.str status]))] |
77 else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
95 else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; |
|
96 val tsymbs = |
78 val tsymbs = |
97 if null tags orelse not show_tags then [] |
79 if null tags orelse not show_tags then [] |
98 else [Pretty.brk 1, pretty_tags tags]; |
80 else [Pretty.brk 1, pretty_tags tags]; |
99 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
81 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
100 |
82 |
101 fun pretty_thm_aux ctxt show_status = |
83 fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
102 pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status}; |
|
103 |
|
104 fun pretty_thm ctxt = pretty_thm_aux ctxt true; |
|
105 |
84 |
106 fun pretty_thm_global thy = |
85 fun pretty_thm_global thy = |
107 pretty_thm_raw (Syntax.init_pretty_global thy) |
86 pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; |
108 {quote = false, show_hyps = false, show_status = true}; |
|
109 |
87 |
110 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; |
88 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; |
111 |
89 |
112 val string_of_thm = Pretty.string_of oo pretty_thm; |
90 val string_of_thm = Pretty.string_of oo pretty_thm; |
113 val string_of_thm_global = Pretty.string_of oo pretty_thm_global; |
91 val string_of_thm_global = Pretty.string_of oo pretty_thm_global; |
114 val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context; |
92 val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context; |
115 |
93 |
116 |
94 |
117 (* multiple theorems *) |
95 (* multiple theorems *) |
118 |
96 |
119 fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th |
97 fun pretty_thms ctxt [th] = pretty_thm ctxt th |
120 | pretty_thms_aux ctxt flag ths = |
98 | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); |
121 Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths)); |
|
122 |
|
123 fun pretty_thms ctxt = pretty_thms_aux ctxt true; |
|
124 |
99 |
125 |
100 |
126 |
101 |
127 (** print theory **) |
102 (** print theory **) |
128 |
103 |