Interface to access the specification of a named locale.

--- a/src/Pure/Isar/locale.ML	Fri Jan 27 05:46:39 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Jan 27 16:05:23 2006 +0100
@@ -43,6 +43,15 @@
   val extern: theory -> string -> xstring
   val init: string -> theory -> Proof.context
 
+  (* The specification of a locale *)
+
+  val parameters_of: theory -> string ->
+    (string * typ option * mixfix) list
+  val local_asms_of: theory -> string ->
+    ((string * Attrib.src list) * term list) list
+  val global_asms_of: theory -> string ->
+    ((string * Attrib.src list) * term list) list
+
   (* Processing of locale statements *)  (* FIXME export more abstract version *)
   val read_context_statement: xstring option -> Element.context element list ->
     (string * (string list * string list)) list list -> Proof.context ->
@@ -1253,6 +1262,42 @@
 end;
 
 
+(* Get the specification of a locale *)
+
+(* The global specification is made from the parameters and global
+   assumptions, the local specification from the parameters and the local
+   assumptions. *)
+
+local
+
+fun gen_asms_of get thy name =
+  let
+    val ctxt = ProofContext.init thy;
+    val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
+    val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
+  in
+    elemss |> map (fn (_, es) => map (fn Int e => e) es)
+      |> Library.flat
+      |> Library.mapfilter (fn Assumes asms => SOME asms | _ => NONE)
+      |> get
+      |> map (apsnd (map fst))
+  end;
+
+in
+
+fun parameters_of thy name =
+  the_locale thy name |> #params |> #1
+    |> map (fn ((p, T), mix) => (p, SOME T, mix));
+
+fun local_asms_of thy name =
+  gen_asms_of Library.last_elem thy name;
+
+fun global_asms_of thy name =
+  gen_asms_of Library.flat thy name;
+
+end (* local *)
+
+
 (* full context statements: import + elements + conclusion *)
 
 local