added pprint_thy_ref;
authorwenzelm
Tue Jun 24 19:43:17 2008 +0200 (2008-06-24)
changeset 2734197e2ccba3b64
parent 27340 3de9f20f4e28
child 27342 3945da15d410
added pprint_thy_ref;
src/Pure/context.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/context.ML	Tue Jun 24 19:43:16 2008 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Jun 24 19:43:17 2008 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val pretty_thy: theory -> Pretty.T
     1.5    val string_of_thy: theory -> string
     1.6    val pprint_thy: theory -> pprint_args -> unit
     1.7 +  val pprint_thy_ref: theory_ref -> pprint_args -> unit
     1.8    val pretty_abbrev_thy: theory -> Pretty.T
     1.9    val str_of_thy: theory -> string
    1.10    val deref: theory_ref -> theory
    1.11 @@ -242,6 +243,8 @@
    1.12      else thy_ref
    1.13    end;
    1.14  
    1.15 +val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
    1.16 +
    1.17  
    1.18  (* consistency *)
    1.19  
     2.1 --- a/src/Pure/pure_setup.ML	Tue Jun 24 19:43:16 2008 +0200
     2.2 +++ b/src/Pure/pure_setup.ML	Tue Jun 24 19:43:17 2008 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4  install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
     2.5  install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
     2.6  install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
     2.7 +install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
     2.8  install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
     2.9  install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    2.10  install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));