--- a/NEWS Thu Sep 01 23:08:15 2005 +0200
+++ b/NEWS Fri Sep 02 09:50:58 2005 +0200
@@ -261,6 +261,9 @@
alternative context used for evaluating and printing the subsequent
argument, as in @{thm [locale=LC] fold_commute}, for example.
+* Locale inspection command 'print_locale' omits notes elements. Use
+'print_locale!' to have them included in the output.
+
*** Provers ***
--- a/doc-src/IsarRef/generic.tex Thu Sep 01 23:08:15 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Sep 02 09:50:58 2005 +0200
@@ -114,7 +114,7 @@
\begin{rail}
'locale' ('(open)')? name ('=' localeexpr)?
;
- printlocale localeexpr
+ printlocale '!'? localeexpr
;
localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
;
@@ -224,7 +224,9 @@
expression in a flattened form. The notable special case
$\isarkeyword{print_locale}~loc$ just prints the contents of the named
locale, but keep in mind that type-inference will normalize type variables
- according to the usual alphabetical order.
+ according to the usual alphabetical order. The command omits
+ $\isarkeyword{notes}$ elements by default. Use
+ $\isarkeyword{print_locale}!$ to get them included.
\item [$\isarkeyword{print_locales}$] prints the names of all locales of the
current theory.
--- a/src/FOL/ex/LocaleTest.thy Thu Sep 01 23:08:15 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy Fri Sep 02 09:50:58 2005 +0200
@@ -421,8 +421,8 @@
(* effect on printed locale *)
-print_locale Rrgrp
-print_locale Rlgrp
+print_locale! Rrgrp
+print_locale! Rlgrp
(* locale with many parameters ---
interpretations generate alternating group A5 *)
--- a/src/Pure/Isar/isar_cmd.ML Thu Sep 01 23:08:15 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Sep 02 09:50:58 2005 +0200
@@ -47,7 +47,7 @@
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 * Locale.element list
+ val print_locale: bool * (Locale.expr * Locale.element list)
-> Toplevel.transition -> Toplevel.transition
val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
@@ -228,8 +228,8 @@
val print_locales = Toplevel.unknown_theory o
Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
-fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Locale.print_locale (Toplevel.theory_of state) import body);
+fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ Locale.print_locale (Toplevel.theory_of state) show_facts import body);
fun print_registrations show_wits name = Toplevel.unknown_context o
Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations show_wits name)
--- a/src/Pure/Isar/isar_syn.ML Thu Sep 01 23:08:15 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Sep 02 09:50:58 2005 +0200
@@ -643,7 +643,7 @@
val print_localeP =
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
- (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
+ (Scan.optional (P.$$$ "!" >> K true) false -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
val print_registrationsP =
OuterSyntax.improper_command "print_interps"
--- a/src/Pure/Isar/locale.ML Thu Sep 01 23:08:15 2005 +0200
+++ b/src/Pure/Isar/locale.ML Fri Sep 02 09:50:58 2005 +0200
@@ -67,7 +67,7 @@
(* Diagnostic functions *)
val print_locales: theory -> unit
- val print_locale: theory -> expr -> element list -> unit
+ val print_locale: theory -> bool -> expr -> element list -> unit
val print_global_registrations: bool -> string -> theory -> unit
val print_local_registrations': bool -> string -> context -> unit
val print_local_registrations: bool -> string -> context -> unit
@@ -1620,7 +1620,7 @@
(* print locale *)
-fun print_locale thy import body =
+fun print_locale thy show_facts import body =
let
val thy_ctxt = ProofContext.init thy;
val (((_, import_elemss), (ctxt, elemss, _)), _) = read_context import body thy_ctxt;
@@ -1661,7 +1661,8 @@
| prt_elem (Constrains csts) = items "constrains" (map prt_cst csts)
| prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
| prt_elem (Defines defs) = items "defines" (map prt_def defs)
- | prt_elem (Notes facts) = items "notes" (map prt_note facts);
+ | prt_elem (Notes facts) =
+ if show_facts then items "notes" (map prt_note facts) else [];
in
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
|> Pretty.writeln
@@ -1974,11 +1975,17 @@
error ("Duplicate definition of locale " ^ quote name));
val thy_ctxt = ProofContext.init thy;
- val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
+ val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
+ text as (parms, ((_, exts'), _), _)) =
prep_ctxt raw_import raw_body thy_ctxt;
val elemss = import_elemss @ body_elemss;
val import = prep_expr thy raw_import;
+ val extraTs = foldr Term.add_term_tfrees [] exts' \\
+ foldr Term.add_typ_tfrees [] (map #2 parms);
+ val _ = if null extraTs then ()
+ else warning ("Encountered type variables in specification text that don't occur in the\n" ^ "locale parameters.");
+
val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
if do_pred then thy |> define_preds bname text elemss
else (thy, (elemss, ([], [])));