equal
deleted
inserted
replaced
209 NONE => [] |
209 NONE => [] |
210 | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
210 | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
211 | SOME (Proof (prf, _)) => |
211 | SOME (Proof (prf, _)) => |
212 Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
212 Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
213 | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |
213 | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |
214 |> Pretty.markup_chunks Isabelle_Markup.state |> Pretty.writeln; |
214 |> Pretty.markup_chunks Markup.state |> Pretty.writeln; |
215 |
215 |
216 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
216 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
217 |
217 |
218 |
218 |
219 |
219 |