toplevel pp for Proof.state and Toplevel.state;
authorwenzelm
Tue Jul 20 20:56:28 2010 +0200 (2010-07-20 ago)
changeset 37858e1ef6b441fe7
parent 37857 4e4b8c0dc766
child 37859 575a14dd4167
toplevel pp for Proof.state and Toplevel.state;
src/Pure/Isar/toplevel.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 20:10:27 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 20:56:28 2010 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val enter_proof_body: state -> Proof.state
     1.5    val print_state_context: state -> unit
     1.6    val print_state: bool -> state -> unit
     1.7 +  val pretty_abstract: state -> Pretty.T
     1.8    val quiet: bool Unsynchronized.ref
     1.9    val debug: bool Unsynchronized.ref
    1.10    val interact: bool Unsynchronized.ref
    1.11 @@ -212,6 +213,8 @@
    1.12    | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    1.13    |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    1.14  
    1.15 +fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    1.16 +
    1.17  
    1.18  
    1.19  (** toplevel transitions **)
     2.1 --- a/src/Pure/pure_setup.ML	Tue Jul 20 20:10:27 2010 +0200
     2.2 +++ b/src/Pure/pure_setup.ML	Tue Jul 20 20:56:28 2010 +0200
     2.3 @@ -34,6 +34,8 @@
     2.4  toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
     2.5  toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
     2.6  toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
     2.7 +toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
     2.8 +toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
     2.9  
    2.10  if ml_system = "polyml-5.3.0"
    2.11  then use "ML-Systems/install_pp_polyml-5.3.ML"