25 struct |
25 struct |
26 |
26 |
27 (* toplevel pretty printing *) |
27 (* toplevel pretty printing *) |
28 |
28 |
29 fun pp_context ctxt = |
29 fun pp_context ctxt = |
30 (if ! ProofContext.debug then |
30 (if ! Proof_Context.debug then |
31 Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt)) |
31 Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt)) |
32 else Pretty.str "<context>"); |
32 else Pretty.str "<context>"); |
33 |
33 |
34 fun pp_thm th = |
34 fun pp_thm th = |
35 let |
35 let |
36 val thy = Thm.theory_of_thm th; |
36 val thy = Thm.theory_of_thm th; |
46 |
46 |
47 (* theorems and theory *) |
47 (* theorems and theory *) |
48 |
48 |
49 fun pretty_theorems_diff verbose prev_thys thy = |
49 fun pretty_theorems_diff verbose prev_thys thy = |
50 let |
50 let |
51 val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy); |
51 val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy); |
52 val facts = Global_Theory.facts_of thy; |
52 val facts = Global_Theory.facts_of thy; |
53 val thmss = |
53 val thmss = |
54 Facts.dest_static (map Global_Theory.facts_of prev_thys) facts |
54 Facts.dest_static (map Global_Theory.facts_of prev_thys) facts |
55 |> not verbose ? filter_out (Facts.is_concealed facts o #1); |
55 |> not verbose ? filter_out (Facts.is_concealed facts o #1); |
56 in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end; |
56 in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end; |
85 Pretty.block [Pretty.command kind, Pretty.brk 1, |
85 Pretty.block [Pretty.command kind, Pretty.brk 1, |
86 Pretty.str (Long_Name.base_name name), Pretty.str ":"]; |
86 Pretty.str (Long_Name.base_name name), Pretty.str ":"]; |
87 |
87 |
88 fun pretty_facts ctxt = |
88 fun pretty_facts ctxt = |
89 flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o |
89 flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o |
90 map (single o ProofContext.pretty_fact_aux ctxt false); |
90 map (single o Proof_Context.pretty_fact_aux ctxt false); |
91 |
91 |
92 in |
92 in |
93 |
93 |
94 fun print_results do_print ctxt ((kind, name), facts) = |
94 fun print_results do_print ctxt ((kind, name), facts) = |
95 if not do_print orelse kind = "" then () |
95 if not do_print orelse kind = "" then () |
96 else if name = "" then |
96 else if name = "" then |
97 Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts)) |
97 Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts)) |
98 else Pretty.writeln |
98 else Pretty.writeln |
99 (case facts of |
99 (case facts of |
100 [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, |
100 [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, |
101 ProofContext.pretty_fact_aux ctxt false fact]) |
101 Proof_Context.pretty_fact_aux ctxt false fact]) |
102 | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, |
102 | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, |
103 Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); |
103 Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); |
104 |
104 |
105 end; |
105 end; |
106 |
106 |
116 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); |
116 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); |
117 |
117 |
118 in |
118 in |
119 |
119 |
120 fun pretty_consts ctxt pred cs = |
120 fun pretty_consts ctxt pred cs = |
121 (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of |
121 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of |
122 [] => pretty_vars ctxt "constants" cs |
122 [] => pretty_vars ctxt "constants" cs |
123 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
123 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
124 |
124 |
125 end; |
125 end; |
126 |
126 |