--- a/NEWS Tue May 03 22:26:16 2011 +0200
+++ b/NEWS Tue May 03 22:27:32 2011 +0200
@@ -37,12 +37,16 @@
Note that automated detection from the file-system or search path has
been discontinued. INCOMPATIBILITY.
-* Name space: proper configuration options "long_names",
-"short_names", "unique_names" instead of former unsynchronized
-references. Minor INCOMPATIBILITY, need to declare options in context
-like this:
-
- declare [[unique_names = false]]
+* Name space: former unsynchronized references are now proper
+configuration options, with more conventional names:
+
+ long_names ~> names_long
+ short_names ~> names_short
+ unique_names ~> names_unique
+
+Minor INCOMPATIBILITY, need to declare options in context like this:
+
+ declare [[names_unique = false]]
* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note
that the result needs to be unique, which means fact specifications
--- a/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:27:32 2011 +0200
@@ -22,6 +22,6 @@
setup {* Code_Target.set_default_code_width 74 *}
-declare [[unique_names = false]]
+declare [[names_unique = false]]
end
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:27:32 2011 +0200
@@ -341,16 +341,16 @@
\item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
controls folding of abbreviations.
- \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
+ \item @{antiquotation_option_def names_long}~@{text "= bool"} forces
names of types and constants etc.\ to be printed in their fully
qualified internal form.
- \item @{antiquotation_option_def short_names}~@{text "= bool"}
+ \item @{antiquotation_option_def names_short}~@{text "= bool"}
forces names of types and constants etc.\ to be printed unqualified.
Note that internalizing the output again in the current context may
well yield a different result.
- \item @{antiquotation_option_def unique_names}~@{text "= bool"}
+ \item @{antiquotation_option_def names_unique}~@{text "= bool"}
determines whether the printed version of qualified names should be
made sufficiently long to avoid overlap with names declared further
back. Set to @{text false} for more concise output.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:27:32 2011 +0200
@@ -100,9 +100,9 @@
@{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
@{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
@{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
- @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
- @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
- @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
+ @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
@{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
@{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
@{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
@@ -144,8 +144,8 @@
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item @{attribute long_names}, @{attribute short_names}, and
- @{attribute unique_names} control the way of printing fully
+ \item @{attribute names_long}, @{attribute names_short}, and
+ @{attribute names_unique} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:27:32 2011 +0200
@@ -497,16 +497,16 @@
\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
+ \item \indexdef{}{antiquotation option}{names\_long}\hypertarget{antiquotation option.names-long}{\hyperlink{antiquotation option.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}}~\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.
- \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
+ \item \indexdef{}{antiquotation option}{names\_short}\hypertarget{antiquotation option.names-short}{\hyperlink{antiquotation option.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
forces names of types and constants etc.\ to be printed unqualified.
Note that internalizing the output again in the current context may
well yield a different result.
- \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
+ \item \indexdef{}{antiquotation option}{names\_unique}\hypertarget{antiquotation option.names-unique}{\hyperlink{antiquotation option.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
determines whether the printed version of qualified names should be
made sufficiently long to avoid overlap with names declared further
back. Set to \isa{false} for more concise output.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:27:32 2011 +0200
@@ -175,9 +175,9 @@
\indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
\indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
+ \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
\indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\
@@ -219,8 +219,8 @@
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
- \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
+ \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and
+ \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:27:32 2011 +0200
@@ -152,7 +152,7 @@
the qualified name, for example @{text "T.length"}, where @{text T} is the
theory it is defined in, to distinguish it from the predefined @{const[source]
"List.length"}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!short_names!
+short names (no qualifiers) by setting the \verb!names_short!
configuration option in the context.
*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:27:32 2011 +0200
@@ -195,7 +195,7 @@
If there are multiple declarations of the same name, Isabelle prints
the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!short_names!
+short names (no qualifiers) by setting the \verb!names_short!
configuration option in the context.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:27:32 2011 +0200
@@ -2,7 +2,7 @@
theory Itrev
imports Main
begin
-declare [[unique_names = false]]
+declare [[names_unique = false]]
(*>*)
section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
\index{induction heuristics|)}
*}
(*<*)
-declare [[unique_names = true]]
+declare [[names_unique = true]]
end
(*>*)
--- a/src/Pure/General/name_space.ML Tue May 03 22:26:16 2011 +0200
+++ b/src/Pure/General/name_space.ML Tue May 03 22:27:32 2011 +0200
@@ -20,15 +20,15 @@
val markup: T -> string -> Markup.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
- val long_names_default: bool Unsynchronized.ref
- val long_names_raw: Config.raw
- val long_names: bool Config.T
- val short_names_default: bool Unsynchronized.ref
- val short_names_raw: Config.raw
- val short_names: bool Config.T
- val unique_names_default: bool Unsynchronized.ref
- val unique_names_raw: Config.raw
- val unique_names: bool Config.T
+ val names_long_default: bool Unsynchronized.ref
+ val names_long_raw: Config.raw
+ val names_long: bool Config.T
+ val names_short_default: bool Unsynchronized.ref
+ val names_short_raw: Config.raw
+ val names_short: bool Config.T
+ val names_unique_default: bool Unsynchronized.ref
+ val names_unique_raw: Config.raw
+ val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
val hide: bool -> string -> T -> T
val merge: T * T -> T
@@ -161,33 +161,33 @@
fun intern space xname = #1 (lookup space xname);
-val long_names_default = Unsynchronized.ref false;
-val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
-val long_names = Config.bool long_names_raw;
+val names_long_default = Unsynchronized.ref false;
+val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
+val names_long = Config.bool names_long_raw;
-val short_names_default = Unsynchronized.ref false;
-val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
-val short_names = Config.bool short_names_raw;
+val names_short_default = Unsynchronized.ref false;
+val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
+val names_short = Config.bool names_short_raw;
-val unique_names_default = Unsynchronized.ref true;
-val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
-val unique_names = Config.bool unique_names_raw;
+val names_unique_default = Unsynchronized.ref true;
+val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
+val names_unique = Config.bool names_unique_raw;
fun extern ctxt space name =
let
- val long_names = Config.get ctxt long_names;
- val short_names = Config.get ctxt short_names;
- val unique_names = Config.get ctxt unique_names;
+ val names_long = Config.get ctxt names_long;
+ val names_short = Config.get ctxt names_short;
+ val names_unique = Config.get ctxt names_unique;
fun valid require_unique xname =
let val (name', is_unique) = lookup space xname
in name = name' andalso (not require_unique orelse is_unique) end;
fun ext [] = if valid false name then name else hidden name
- | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
+ | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
in
- if long_names then name
- else if short_names then Long_Name.base_name name
+ if names_long then name
+ else if names_short then Long_Name.base_name name
else ext (get_accesses space name)
end;
--- a/src/Pure/Isar/attrib.ML Tue May 03 22:26:16 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Tue May 03 22:27:32 2011 +0200
@@ -441,9 +441,9 @@
register_config Printer.show_question_marks_raw #>
register_config Syntax.ambiguity_level_raw #>
register_config Syntax_Trans.eta_contract_raw #>
- register_config Name_Space.long_names_raw #>
- register_config Name_Space.short_names_raw #>
- register_config Name_Space.unique_names_raw #>
+ register_config Name_Space.names_long_raw #>
+ register_config Name_Space.names_short_raw #>
+ register_config Name_Space.names_unique_raw #>
register_config ML_Context.trace_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
--- a/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:26:16 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:27:32 2011 +0200
@@ -124,7 +124,7 @@
bool_pref Goal_Display.show_consts_default
"show-consts"
"Show types of consts in Isabelle goal display",
- bool_pref Name_Space.long_names_default
+ bool_pref Name_Space.names_long_default
"long-names"
"Show fully qualified names in Isabelle terms",
bool_pref Printer.show_brackets_default
--- a/src/Pure/Thy/thy_output.ML Tue May 03 22:26:16 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue May 03 22:27:32 2011 +0200
@@ -450,9 +450,9 @@
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" (Config.put Name_Space.long_names o boolean);
-val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
-val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
+val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
+val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
+val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
val _ = add_option "display" (Config.put display o boolean);
val _ = add_option "break" (Config.put break o boolean);
--- a/src/Pure/Tools/find_theorems.ML Tue May 03 22:26:16 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue May 03 22:27:32 2011 +0200
@@ -383,9 +383,9 @@
val shorten =
Name_Space.extern
(ctxt
- |> Config.put Name_Space.long_names false
- |> Config.put Name_Space.short_names false
- |> Config.put Name_Space.unique_names false) space;
+ |> Config.put Name_Space.names_long false
+ |> Config.put Name_Space.names_short false
+ |> Config.put Name_Space.names_unique false) space;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
nicer_name (shorten x, i) (shorten y, j)