# HG changeset patch # User ballarin # Date 1125647458 -7200 # Node ID 19b460b39dad673f6a7cf37484580294d9ee1de0 # Parent 398a7353ca6966d9c72b1e1487d3a69a65d34696 print_locale omits facts by default diff -r 398a7353ca69 -r 19b460b39dad NEWS --- 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 *** diff -r 398a7353ca69 -r 19b460b39dad doc-src/IsarRef/generic.tex --- 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. diff -r 398a7353ca69 -r 19b460b39dad src/FOL/ex/LocaleTest.thy --- 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 *) diff -r 398a7353ca69 -r 19b460b39dad src/Pure/Isar/isar_cmd.ML --- 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) diff -r 398a7353ca69 -r 19b460b39dad src/Pure/Isar/isar_syn.ML --- 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" diff -r 398a7353ca69 -r 19b460b39dad src/Pure/Isar/locale.ML --- 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, ([], [])));