added query_type/const/class (meta data);
authorwenzelm
Sat Jun 21 16:18:51 2008 +0200 (2008-06-21 ago)
changeset 27314fce7f0c7cf76
parent 27313 07754b7ba89d
child 27315 5d24085e0858
added query_type/const/class (meta data);
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jun 21 16:18:50 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jun 21 16:18:51 2008 +0200
     1.3 @@ -145,6 +145,9 @@
     1.4    val prems_limit: int ref
     1.5    val pretty_ctxt: Proof.context -> Pretty.T list
     1.6    val pretty_context: Proof.context -> Pretty.T list
     1.7 +  val query_type: Proof.context -> string -> Markup.property list
     1.8 +  val query_const: Proof.context -> string -> Markup.property list
     1.9 +  val query_class: Proof.context -> string -> Markup.property list
    1.10  end;
    1.11  
    1.12  structure ProofContext: PROOF_CONTEXT =
    1.13 @@ -1334,4 +1337,14 @@
    1.14      verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
    1.15    end;
    1.16  
    1.17 +
    1.18 +(* query meta data *)
    1.19 +
    1.20 +val query_type = Type.the_tags o tsig_of;
    1.21 +
    1.22 +fun query_const ctxt name =
    1.23 +  Consts.the_tags (consts_of ctxt) name handle TYPE (msg, _, _) => error msg;
    1.24 +
    1.25 +fun query_class ctxt name = query_const ctxt (Logic.const_of_class name);
    1.26 +
    1.27  end;