--- a/src/Pure/Isar/toplevel.ML Tue Jul 20 20:10:27 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jul 20 20:56:28 2010 +0200
@@ -24,6 +24,7 @@
val enter_proof_body: state -> Proof.state
val print_state_context: state -> unit
val print_state: bool -> state -> unit
+ val pretty_abstract: state -> Pretty.T
val quiet: bool Unsynchronized.ref
val debug: bool Unsynchronized.ref
val interact: bool Unsynchronized.ref
@@ -212,6 +213,8 @@
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
|> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
+
(** toplevel transitions **)