print_locale: allow full body specification;

--- a/src/Pure/Isar/isar_cmd.ML	Tue Jan 15 00:09:54 2002 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jan 15 00:11:30 2002 +0100
@@ -47,7 +47,8 @@
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: Locale.expr -> Toplevel.transition -> Toplevel.transition
+  val print_locale: Locale.expr * (Args.src Locale.element * Comment.text) list
+    -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_rules: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
@@ -193,8 +194,11 @@
 val print_locales = Toplevel.unknown_theory o
   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
 
-fun print_locale name = Toplevel.unknown_theory o
-  Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) name);
+fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  let val thy = Toplevel.theory_of state in
+    Locale.print_locale thy import
+      (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body)
+  end);
 
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);

--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 15 00:09:54 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 15 00:11:30 2002 +0100
@@ -286,15 +286,14 @@
 
 (* locales *)
 
-val locale_decl =
-  (P.name --| P.$$$ "=") --
-    (P.locale_expr -- Scan.optional
-      (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
-    Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty) >> P.triple2;
+val locale_val =
+  (P.locale_expr --
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
+  Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty);
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (locale_decl >> (Toplevel.theory o IsarThy.add_locale));
+    ((P.name --| P.$$$ "=") -- locale_val >> (Toplevel.theory o IsarThy.add_locale o P.triple2));
 
 
 
@@ -563,7 +562,7 @@
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print named locale of this theory" K.diag
-    (P.locale_expr >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_attributesP =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag

--- a/src/Pure/Isar/locale.ML	Tue Jan 15 00:09:54 2002 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Jan 15 00:11:30 2002 +0100
@@ -42,10 +42,10 @@
   val cert_context_statement: string option -> context attribute element_i list ->
     (term * (term list * term list)) list list -> context ->
     string option * context * context * (term * (term list * term list)) list list
+  val print_locales: theory -> unit
+  val print_locale: theory -> expr -> context attribute element list -> unit
   val add_locale: bstring -> expr -> context attribute element list -> theory -> theory
   val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory
-  val print_locales: theory -> unit
-  val print_locale: theory -> expr -> unit
   val have_thmss: string -> xstring ->
     ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
@@ -694,11 +694,13 @@
 
 (** print locale **)
 
-fun print_locale thy raw_expr =
+fun print_locale thy import body =
   let
     val sg = Theory.sign_of thy;
     val thy_ctxt = ProofContext.init thy;
-    val (((ctxt, elemss), _), ((_, (pred_xs, pred_ts)), _)) = read_context raw_expr [] thy_ctxt;
+    val (((_, import_elemss), (ctxt, elemss)), ((_, (pred_xs, pred_ts)), _)) =
+      read_context import body thy_ctxt;
+    val all_elems = flat (map #2 (import_elemss @ elemss));
 
     val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
@@ -733,7 +735,7 @@
         |> curry Term.list_abs_free pred_xs
         |> prt_term;
   in
-    [Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) (flat (map #2 elemss))),
+    [Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems),
       Pretty.big_list "predicate text:" [prt_pred]] |> Pretty.chunks |> Pretty.writeln
   end;