src/Pure/Thy/thy_output.ML
changeset 39305 d4fa19eb0822
parent 39134 917b4b6ba3d2
child 39308 c2c9bb3c52c6
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Sep 13 09:29:43 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Sep 13 14:53:56 2010 +0200
     1.3 @@ -507,6 +507,12 @@
     1.4      val ctxt' = Variable.auto_fixes eq ctxt;
     1.5    in ProofContext.pretty_term_abbrev ctxt' eq end;
     1.6  
     1.7 +fun pretty_class ctxt =
     1.8 +  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
     1.9 +
    1.10 +fun pretty_type ctxt = Pretty.str o Type.extern_type (ProofContext.tsig_of ctxt)
    1.11 +  o fst o dest_Type o ProofContext.read_type_name_proper ctxt false;
    1.12 +
    1.13  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    1.14  
    1.15  fun pretty_theory ctxt name =
    1.16 @@ -561,6 +567,8 @@
    1.17  val _ = basic_entity "const" (Args.const_proper false) pretty_const;
    1.18  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
    1.19  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
    1.20 +val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
    1.21 +val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
    1.22  val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
    1.23  val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
    1.24  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);