20 val generic_theory_of: state -> generic_theory |
20 val generic_theory_of: state -> generic_theory |
21 val theory_of: state -> theory |
21 val theory_of: state -> theory |
22 val proof_of: state -> Proof.state |
22 val proof_of: state -> Proof.state |
23 val proof_position_of: state -> int |
23 val proof_position_of: state -> int |
24 val end_theory: Position.T -> state -> theory |
24 val end_theory: Position.T -> state -> theory |
25 val print_state_context: state -> unit |
25 val pretty_state_context: state -> Pretty.T list |
|
26 val pretty_state: bool -> state -> Pretty.T list |
26 val print_state: bool -> state -> unit |
27 val print_state: bool -> state -> unit |
27 val pretty_abstract: state -> Pretty.T |
28 val pretty_abstract: state -> Pretty.T |
28 val quiet: bool Unsynchronized.ref |
29 val quiet: bool Unsynchronized.ref |
29 val interact: bool Unsynchronized.ref |
30 val interact: bool Unsynchronized.ref |
30 val timing: bool Unsynchronized.ref |
31 val timing: bool Unsynchronized.ref |
197 |
198 |
198 (* print state *) |
199 (* print state *) |
199 |
200 |
200 val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; |
201 val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; |
201 |
202 |
202 fun print_state_context state = |
203 fun pretty_state_context state = |
203 (case try node_of state of |
204 (case try node_of state of |
204 NONE => [] |
205 NONE => [] |
205 | SOME (Theory (gthy, _)) => pretty_context gthy |
206 | SOME (Theory (gthy, _)) => pretty_context gthy |
206 | SOME (Proof (_, (_, gthy))) => pretty_context gthy |
207 | SOME (Proof (_, (_, gthy))) => pretty_context gthy |
207 | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy) |
208 | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy); |
208 |> Pretty.writeln_chunks; |
209 |
209 |
210 fun pretty_state prf_only state = |
210 fun print_state prf_only state = |
|
211 (case try node_of state of |
211 (case try node_of state of |
212 NONE => [] |
212 NONE => [] |
213 | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
213 | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
214 | SOME (Proof (prf, _)) => |
214 | SOME (Proof (prf, _)) => |
215 Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
215 Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
216 | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |
216 | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); |
217 |> Pretty.markup_chunks Markup.state |> Pretty.writeln; |
217 |
|
218 fun print_state prf_only = |
|
219 pretty_state prf_only #> Pretty.markup_chunks Markup.state #> Pretty.writeln; |
218 |
220 |
219 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
221 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
220 |
222 |
221 |
223 |
222 |
224 |