# HG changeset patch
# User wenzelm
# Date 1214057931 -7200
# Node ID fce7f0c7cf7685bf3c71bf425193eaa506bc5752
# Parent  07754b7ba89d0ccd37f0fd686b8348b5364cca32
added query_type/const/class (meta data);

diff -r 07754b7ba89d -r fce7f0c7cf76 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jun 21 16:18:50 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 21 16:18:51 2008 +0200
@@ -145,6 +145,9 @@
   val prems_limit: int ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
+  val query_type: Proof.context -> string -> Markup.property list
+  val query_const: Proof.context -> string -> Markup.property list
+  val query_class: Proof.context -> string -> Markup.property list
 end;
 
 structure ProofContext: PROOF_CONTEXT =
@@ -1334,4 +1337,14 @@
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
+
+(* query meta data *)
+
+val query_type = Type.the_tags o tsig_of;
+
+fun query_const ctxt name =
+  Consts.the_tags (consts_of ctxt) name handle TYPE (msg, _, _) => error msg;
+
+fun query_class ctxt name = query_const ctxt (Logic.const_of_class name);
+
 end;