# HG changeset patch
# User wenzelm
# Date 1279652188 -7200
# Node ID e1ef6b441fe79e9d1e2e960c9a8d8bbdc88a3993
# Parent  4e4b8c0dc76627f1ddc6430d8b2d9f1a28bf12c0
toplevel pp for Proof.state and Toplevel.state;

diff -r 4e4b8c0dc766 -r e1ef6b441fe7 src/Pure/Isar/toplevel.ML
--- 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 **)
diff -r 4e4b8c0dc766 -r e1ef6b441fe7 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Jul 20 20:10:27 2010 +0200
+++ b/src/Pure/pure_setup.ML	Tue Jul 20 20:56:28 2010 +0200
@@ -34,6 +34,8 @@
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
+toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
+toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
 if ml_system = "polyml-5.3.0"
 then use "ML-Systems/install_pp_polyml-5.3.ML"