--- a/NEWS Thu Dec 02 11:18:44 2010 -0800
+++ b/NEWS Thu Dec 02 21:04:20 2010 +0100
@@ -34,8 +34,8 @@
* Various options that affect pretty printing etc. are now properly
handled within the context via configuration options, instead of
-unsynchronized references. There are both ML Config.T entities and
-Isar declaration attributes to access these.
+unsynchronized references or print modes. There are both ML Config.T
+entities and Isar declaration attributes to access these.
ML (Config.T) Isar (attribute)
@@ -45,6 +45,7 @@
show_types show_types
show_question_marks show_question_marks
show_consts show_consts
+ show_abbrevs show_abbrevs
Syntax.ambiguity_level syntax_ambiguity_level
@@ -59,6 +60,14 @@
Note that corresponding "..._default" references in ML may be only
changed globally at the ROOT session setup, but *not* within a theory.
+The option "show_abbrevs" supersedes the former print mode
+"no_abbrevs" with inverted meaning.
+
+* More systematic naming of some configuration options.
+ INCOMPATIBILTY.
+
+ trace_simp ~> simp_trace
+ debug_simp ~> simp_debug
*** Pure ***
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Dec 02 21:04:20 2010 +0100
@@ -339,6 +339,9 @@
\item @{antiquotation_option_def show_structs}~@{text "= bool"}
controls printing of implicit structures.
+ \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
+ controls folding of abbreviations.
+
\item @{antiquotation_option_def long_names}~@{text "= bool"} forces
names of types and constants etc.\ to be printed in their fully
qualified internal form.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 02 21:04:20 2010 +0100
@@ -99,6 +99,7 @@
@{index_ML show_types: "bool Config.T"} & default @{ML false} \\
@{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
@{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
+ @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
@{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
@@ -141,6 +142,8 @@
Note that the output can be enormous, because polymorphic constants
often occur at several different type instances.
+ \item @{ML show_abbrevs} controls folding of constant abbreviations.
+
\item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
control the way of printing fully qualified internal names in
external form. See also \secref{sec:antiq} for the document
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Dec 02 21:04:20 2010 +0100
@@ -357,6 +357,9 @@
\item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}structs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
controls printing of implicit structures.
+ \item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
+ controls folding of abbreviations.
+
\item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces
names of types and constants etc.\ to be printed in their fully
qualified internal form.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 02 21:04:20 2010 +0100
@@ -121,6 +121,7 @@
\indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
+ \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
\indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
@@ -162,6 +163,8 @@
Note that the output can be enormous, because polymorphic constants
often occur at several different type instances.
+ \item \verb|show_abbrevs| controls folding of constant abbreviations.
+
\item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
control the way of printing fully qualified internal names in
external form. See also \secref{sec:antiq} for the document
--- a/doc-src/TutorialI/Misc/simp.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/TutorialI/Misc/simp.thy Thu Dec 02 21:04:20 2010 +0100
@@ -422,7 +422,7 @@
(*<*)lemma "x=x"
(*>*)
-using [[trace_simp=true]]
+using [[simp_trace=true]]
apply simp
(*<*)oops(*>*)
--- a/doc-src/TutorialI/Recdef/Nested2.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Thu Dec 02 21:04:20 2010 +0100
@@ -30,7 +30,7 @@
text{*\noindent
If the proof of the induction step mystifies you, we recommend that you go through
the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
+@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
--- a/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 21:04:20 2010 +0100
@@ -16,8 +16,7 @@
text {* The following abstract syntax and semantics of Hoare Logic
over \texttt{WHILE} programs closely follows the existing tradition
in Isabelle/HOL of formalizing the presentation given in
- \cite[\S6]{Winskel:1993}. See also
- \url{http://isabelle.in.tum.de/library/Hoare/} and
+ \cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and
\cite{Nipkow:1998:Winskel}. *}
types
@@ -364,7 +363,7 @@
text {* We now load the \emph{original} ML file for proof scripts and
tactic definition for the Hoare Verification Condition Generator
- (see \url{http://isabelle.in.tum.de/library/Hoare/}). As far as we
+ (see @{file "~~/src/HOL/Hoare/"}). As far as we
are concerned here, the result is a proof method \name{hoare}, which
may be applied to a Hoare Logic assertion to extract purely logical
verification conditions. It is important to note that the method
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 21:04:20 2010 +0100
@@ -10,9 +10,7 @@
begin
text {* The Mutilated Checker Board Problem, formalized inductively.
- See \cite{paulson-mutilated-board} and
- \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for
- the original tactic script version. *}
+ See \cite{paulson-mutilated-board} for the original tactic script version. *}
subsection {* Tilings *}
--- a/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 11:18:44 2010 -0800
+++ b/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 21:04:20 2010 +0100
@@ -8,11 +8,6 @@
imports Main
begin
-text_raw {* \footnote{This example is somewhat reminiscent of the
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
- discussed in \cite{isabelle-ref} in the context of permutative
- rewrite rules and ordered rewriting.} *}
-
text {* Subsequently, we prove some summation laws of natural numbers
(including odds, squares, and cubes). These examples demonstrate
how plain natural deduction (including induction) may be combined
@@ -126,8 +121,8 @@
qed
text {* Comparing these examples with the tactic script version
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
- an important difference of how induction vs.\ simplification is
+ @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference
+ of how induction vs.\ simplification is
applied. While \cite[\S10]{isabelle-ref} advises for these examples
that ``induction should not be applied until the goal is in the
simplest form'' this would be a very bad idea in our setting.
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Dec 02 21:04:20 2010 +0100
@@ -446,7 +446,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Simp_tac 1));
(*cancel_numerals*)
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 21:04:20 2010 +0100
@@ -764,7 +764,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s, by (Simp_tac 1));
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
@@ -803,7 +803,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Simp_tac 1));
test "9*x = 12 * (y::int)";
@@ -873,7 +873,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::int)";
@@ -890,7 +890,7 @@
(*And the same examples for fields such as rat or real:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::rat)";
--- a/src/Pure/Isar/attrib.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/Pure/Isar/attrib.ML Thu Dec 02 21:04:20 2010 +0100
@@ -405,6 +405,7 @@
register_config Syntax.show_question_marks_raw #>
register_config Syntax.ambiguity_level_raw #>
register_config Syntax.eta_contract_raw #>
+ register_config ProofContext.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
register_config Goal_Display.show_consts_raw #>
@@ -415,7 +416,7 @@
register_config Unify.trace_simp_raw #>
register_config Unify.trace_types_raw #>
register_config MetaSimplifier.simp_depth_limit_raw #>
- register_config MetaSimplifier.debug_simp_raw #>
- register_config MetaSimplifier.trace_simp_raw));
+ register_config MetaSimplifier.simp_debug_raw #>
+ register_config MetaSimplifier.simp_trace_raw));
end;
--- a/src/Pure/Isar/proof_context.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML Thu Dec 02 21:04:20 2010 +0100
@@ -70,6 +70,8 @@
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
+ val show_abbrevs_raw: Config.raw
+ val show_abbrevs: bool Config.T
val expand_abbrevs: Proof.context -> term -> term
val cert_term: Proof.context -> term -> term
val cert_prop: Proof.context -> term -> term
@@ -554,6 +556,8 @@
end;
+val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
+val show_abbrevs = Config.bool show_abbrevs_raw;
fun contract_abbrevs ctxt t =
let
@@ -563,7 +567,7 @@
val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
in
- if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
+ if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
else Pattern.rewrite_term_top thy [] [match_abbrev] t
end;
@@ -1480,3 +1484,5 @@
end;
+val show_abbrevs = ProofContext.show_abbrevs;
+
--- a/src/Pure/ProofGeneral/preferences.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/Pure/ProofGeneral/preferences.ML Thu Dec 02 21:04:20 2010 +0100
@@ -147,10 +147,10 @@
"Show leading question mark of variable name"];
val tracing_preferences =
- [bool_pref trace_simp_default
+ [bool_pref simp_trace_default
"trace-simplifier"
"Trace simplification rules.",
- nat_pref trace_simp_depth_limit
+ nat_pref simp_trace_depth_limit
"trace-simplifier-depth"
"Trace simplifier depth limit.",
bool_pref trace_rules
--- a/src/Pure/Thy/thy_output.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/Pure/Thy/thy_output.ML Thu Dec 02 21:04:20 2010 +0100
@@ -449,6 +449,7 @@
val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
val _ = add_option "show_structs" (Config.put show_structs o boolean);
val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
+val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
--- a/src/Pure/meta_simplifier.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/Pure/meta_simplifier.ML Thu Dec 02 21:04:20 2010 +0100
@@ -11,12 +11,12 @@
signature BASIC_META_SIMPLIFIER =
sig
- val debug_simp: bool Config.T
- val debug_simp_raw: Config.raw
- val trace_simp: bool Config.T
- val trace_simp_raw: Config.raw
- val trace_simp_default: bool Unsynchronized.ref
- val trace_simp_depth_limit: int Unsynchronized.ref
+ val simp_debug: bool Config.T
+ val simp_debug_raw: Config.raw
+ val simp_trace: bool Config.T
+ val simp_trace_raw: Config.raw
+ val simp_trace_default: bool Unsynchronized.ref
+ val simp_trace_depth_limit: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
type simpset
@@ -253,18 +253,18 @@
val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
val simp_depth_limit = Config.int simp_depth_limit_raw;
-val trace_simp_depth_limit = Unsynchronized.ref 1;
+val simp_trace_depth_limit = Unsynchronized.ref 1;
fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
- if depth > ! trace_simp_depth_limit then
- if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
+ if depth > ! simp_trace_depth_limit then
+ if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
else
(tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
(rules, prems, bounds,
(depth + 1,
- if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
+ if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context));
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
@@ -273,12 +273,12 @@
exception SIMPLIFIER of string * thm;
-val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
-val debug_simp = Config.bool debug_simp_raw;
+val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
+val simp_debug = Config.bool simp_debug_raw;
-val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
-val trace_simp = Config.bool trace_simp_raw;
+val simp_trace_default = Unsynchronized.ref false;
+val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
+val simp_trace = Config.bool simp_trace_raw;
fun if_enabled (Simpset ({context, ...}, _)) flag f =
(case context of
@@ -303,27 +303,27 @@
fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
Syntax.string_of_term ctxt
- (if Config.get ctxt debug_simp then t else show_bounds ss t));
+ (if Config.get ctxt simp_debug then t else show_bounds ss t));
in
fun print_term_global ss warn a thy t =
print_term ss warn (K a) t (ProofContext.init_global thy);
-fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
-fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
+fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
-fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
-fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
+fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
fun trace_cterm warn a ss ct =
- if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
+ if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
fun trace_thm a ss th =
- if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
+ if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
fun trace_named_thm a ss (th, name) =
- if_enabled ss trace_simp (print_term ss false
+ if_enabled ss simp_trace (print_term ss false
(fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
(Thm.full_prop_of th));
--- a/src/ZF/arith_data.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/ZF/arith_data.ML Thu Dec 02 21:04:20 2010 +0100
@@ -223,7 +223,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x #+ y = x #+ z";
--- a/src/ZF/int_arith.ML Thu Dec 02 11:18:44 2010 -0800
+++ b/src/ZF/int_arith.ML Thu Dec 02 21:04:20 2010 +0100
@@ -312,7 +312,7 @@
(*
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
val sg = #sign (rep_thm (topthm()));
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));