1.1 --- a/NEWS Tue May 03 22:26:16 2011 +0200
1.2 +++ b/NEWS Tue May 03 22:27:32 2011 +0200
1.3 @@ -37,12 +37,16 @@
1.4 Note that automated detection from the file-system or search path has
1.5 been discontinued. INCOMPATIBILITY.
1.6
1.7 -* Name space: proper configuration options "long_names",
1.8 -"short_names", "unique_names" instead of former unsynchronized
1.9 -references. Minor INCOMPATIBILITY, need to declare options in context
1.10 -like this:
1.11 -
1.12 - declare [[unique_names = false]]
1.13 +* Name space: former unsynchronized references are now proper
1.14 +configuration options, with more conventional names:
1.15 +
1.16 + long_names ~> names_long
1.17 + short_names ~> names_short
1.18 + unique_names ~> names_unique
1.19 +
1.20 +Minor INCOMPATIBILITY, need to declare options in context like this:
1.21 +
1.22 + declare [[names_unique = false]]
1.23
1.24 * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note
1.25 that the result needs to be unique, which means fact specifications
2.1 --- a/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:26:16 2011 +0200
2.2 +++ b/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:27:32 2011 +0200
2.3 @@ -22,6 +22,6 @@
2.4
2.5 setup {* Code_Target.set_default_code_width 74 *}
2.6
2.7 -declare [[unique_names = false]]
2.8 +declare [[names_unique = false]]
2.9
2.10 end
3.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:26:16 2011 +0200
3.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:27:32 2011 +0200
3.3 @@ -341,16 +341,16 @@
3.4 \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
3.5 controls folding of abbreviations.
3.6
3.7 - \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
3.8 + \item @{antiquotation_option_def names_long}~@{text "= bool"} forces
3.9 names of types and constants etc.\ to be printed in their fully
3.10 qualified internal form.
3.11
3.12 - \item @{antiquotation_option_def short_names}~@{text "= bool"}
3.13 + \item @{antiquotation_option_def names_short}~@{text "= bool"}
3.14 forces names of types and constants etc.\ to be printed unqualified.
3.15 Note that internalizing the output again in the current context may
3.16 well yield a different result.
3.17
3.18 - \item @{antiquotation_option_def unique_names}~@{text "= bool"}
3.19 + \item @{antiquotation_option_def names_unique}~@{text "= bool"}
3.20 determines whether the printed version of qualified names should be
3.21 made sufficiently long to avoid overlap with names declared further
3.22 back. Set to @{text false} for more concise output.
4.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:26:16 2011 +0200
4.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:27:32 2011 +0200
4.3 @@ -100,9 +100,9 @@
4.4 @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
4.5 @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
4.6 @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
4.7 - @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
4.8 - @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
4.9 - @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
4.10 + @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
4.11 + @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
4.12 + @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
4.13 @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
4.14 @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
4.15 @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
4.16 @@ -144,8 +144,8 @@
4.17 pretty printed entities may occasionally help to diagnose problems
4.18 with operator priorities, for example.
4.19
4.20 - \item @{attribute long_names}, @{attribute short_names}, and
4.21 - @{attribute unique_names} control the way of printing fully
4.22 + \item @{attribute names_long}, @{attribute names_short}, and
4.23 + @{attribute names_unique} control the way of printing fully
4.24 qualified internal names in external form. See also
4.25 \secref{sec:antiq} for the document antiquotation options of the
4.26 same names.
5.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:26:16 2011 +0200
5.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:27:32 2011 +0200
5.3 @@ -497,16 +497,16 @@
5.4 \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}}}
5.5 controls folding of abbreviations.
5.6
5.7 - \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
5.8 + \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
5.9 names of types and constants etc.\ to be printed in their fully
5.10 qualified internal form.
5.11
5.12 - \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}}}
5.13 + \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}}}
5.14 forces names of types and constants etc.\ to be printed unqualified.
5.15 Note that internalizing the output again in the current context may
5.16 well yield a different result.
5.17
5.18 - \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}}}
5.19 + \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}}}
5.20 determines whether the printed version of qualified names should be
5.21 made sufficiently long to avoid overlap with names declared further
5.22 back. Set to \isa{false} for more concise output.
6.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:26:16 2011 +0200
6.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:27:32 2011 +0200
6.3 @@ -175,9 +175,9 @@
6.4 \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
6.5 \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
6.6 \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
6.7 - \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
6.8 - \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
6.9 - \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
6.10 + \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\
6.11 + \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\
6.12 + \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\
6.13 \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
6.14 \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}}} \\
6.15 \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} \\
6.16 @@ -219,8 +219,8 @@
6.17 pretty printed entities may occasionally help to diagnose problems
6.18 with operator priorities, for example.
6.19
6.20 - \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
6.21 - \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
6.22 + \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and
6.23 + \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully
6.24 qualified internal names in external form. See also
6.25 \secref{sec:antiq} for the document antiquotation options of the
6.26 same names.
7.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:26:16 2011 +0200
7.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:27:32 2011 +0200
7.3 @@ -152,7 +152,7 @@
7.4 the qualified name, for example @{text "T.length"}, where @{text T} is the
7.5 theory it is defined in, to distinguish it from the predefined @{const[source]
7.6 "List.length"}. In case there is no danger of confusion, you can insist on
7.7 -short names (no qualifiers) by setting the \verb!short_names!
7.8 +short names (no qualifiers) by setting the \verb!names_short!
7.9 configuration option in the context.
7.10 *}
7.11
8.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:26:16 2011 +0200
8.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:27:32 2011 +0200
8.3 @@ -195,7 +195,7 @@
8.4 If there are multiple declarations of the same name, Isabelle prints
8.5 the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
8.6 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
8.7 -short names (no qualifiers) by setting the \verb!short_names!
8.8 +short names (no qualifiers) by setting the \verb!names_short!
8.9 configuration option in the context.%
8.10 \end{isamarkuptext}%
8.11 \isamarkuptrue%
9.1 --- a/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:26:16 2011 +0200
9.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:27:32 2011 +0200
9.3 @@ -2,7 +2,7 @@
9.4 theory Itrev
9.5 imports Main
9.6 begin
9.7 -declare [[unique_names = false]]
9.8 +declare [[names_unique = false]]
9.9 (*>*)
9.10
9.11 section{*Induction Heuristics*}
9.12 @@ -141,6 +141,6 @@
9.13 \index{induction heuristics|)}
9.14 *}
9.15 (*<*)
9.16 -declare [[unique_names = true]]
9.17 +declare [[names_unique = true]]
9.18 end
9.19 (*>*)
10.1 --- a/src/Pure/General/name_space.ML Tue May 03 22:26:16 2011 +0200
10.2 +++ b/src/Pure/General/name_space.ML Tue May 03 22:27:32 2011 +0200
10.3 @@ -20,15 +20,15 @@
10.4 val markup: T -> string -> Markup.T
10.5 val is_concealed: T -> string -> bool
10.6 val intern: T -> xstring -> string
10.7 - val long_names_default: bool Unsynchronized.ref
10.8 - val long_names_raw: Config.raw
10.9 - val long_names: bool Config.T
10.10 - val short_names_default: bool Unsynchronized.ref
10.11 - val short_names_raw: Config.raw
10.12 - val short_names: bool Config.T
10.13 - val unique_names_default: bool Unsynchronized.ref
10.14 - val unique_names_raw: Config.raw
10.15 - val unique_names: bool Config.T
10.16 + val names_long_default: bool Unsynchronized.ref
10.17 + val names_long_raw: Config.raw
10.18 + val names_long: bool Config.T
10.19 + val names_short_default: bool Unsynchronized.ref
10.20 + val names_short_raw: Config.raw
10.21 + val names_short: bool Config.T
10.22 + val names_unique_default: bool Unsynchronized.ref
10.23 + val names_unique_raw: Config.raw
10.24 + val names_unique: bool Config.T
10.25 val extern: Proof.context -> T -> string -> xstring
10.26 val hide: bool -> string -> T -> T
10.27 val merge: T * T -> T
10.28 @@ -161,33 +161,33 @@
10.29 fun intern space xname = #1 (lookup space xname);
10.30
10.31
10.32 -val long_names_default = Unsynchronized.ref false;
10.33 -val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
10.34 -val long_names = Config.bool long_names_raw;
10.35 +val names_long_default = Unsynchronized.ref false;
10.36 +val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
10.37 +val names_long = Config.bool names_long_raw;
10.38
10.39 -val short_names_default = Unsynchronized.ref false;
10.40 -val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
10.41 -val short_names = Config.bool short_names_raw;
10.42 +val names_short_default = Unsynchronized.ref false;
10.43 +val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
10.44 +val names_short = Config.bool names_short_raw;
10.45
10.46 -val unique_names_default = Unsynchronized.ref true;
10.47 -val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
10.48 -val unique_names = Config.bool unique_names_raw;
10.49 +val names_unique_default = Unsynchronized.ref true;
10.50 +val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
10.51 +val names_unique = Config.bool names_unique_raw;
10.52
10.53 fun extern ctxt space name =
10.54 let
10.55 - val long_names = Config.get ctxt long_names;
10.56 - val short_names = Config.get ctxt short_names;
10.57 - val unique_names = Config.get ctxt unique_names;
10.58 + val names_long = Config.get ctxt names_long;
10.59 + val names_short = Config.get ctxt names_short;
10.60 + val names_unique = Config.get ctxt names_unique;
10.61
10.62 fun valid require_unique xname =
10.63 let val (name', is_unique) = lookup space xname
10.64 in name = name' andalso (not require_unique orelse is_unique) end;
10.65
10.66 fun ext [] = if valid false name then name else hidden name
10.67 - | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
10.68 + | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
10.69 in
10.70 - if long_names then name
10.71 - else if short_names then Long_Name.base_name name
10.72 + if names_long then name
10.73 + else if names_short then Long_Name.base_name name
10.74 else ext (get_accesses space name)
10.75 end;
10.76
11.1 --- a/src/Pure/Isar/attrib.ML Tue May 03 22:26:16 2011 +0200
11.2 +++ b/src/Pure/Isar/attrib.ML Tue May 03 22:27:32 2011 +0200
11.3 @@ -441,9 +441,9 @@
11.4 register_config Printer.show_question_marks_raw #>
11.5 register_config Syntax.ambiguity_level_raw #>
11.6 register_config Syntax_Trans.eta_contract_raw #>
11.7 - register_config Name_Space.long_names_raw #>
11.8 - register_config Name_Space.short_names_raw #>
11.9 - register_config Name_Space.unique_names_raw #>
11.10 + register_config Name_Space.names_long_raw #>
11.11 + register_config Name_Space.names_short_raw #>
11.12 + register_config Name_Space.names_unique_raw #>
11.13 register_config ML_Context.trace_raw #>
11.14 register_config Proof_Context.show_abbrevs_raw #>
11.15 register_config Goal_Display.goals_limit_raw #>
12.1 --- a/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:26:16 2011 +0200
12.2 +++ b/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:27:32 2011 +0200
12.3 @@ -124,7 +124,7 @@
12.4 bool_pref Goal_Display.show_consts_default
12.5 "show-consts"
12.6 "Show types of consts in Isabelle goal display",
12.7 - bool_pref Name_Space.long_names_default
12.8 + bool_pref Name_Space.names_long_default
12.9 "long-names"
12.10 "Show fully qualified names in Isabelle terms",
12.11 bool_pref Printer.show_brackets_default
13.1 --- a/src/Pure/Thy/thy_output.ML Tue May 03 22:26:16 2011 +0200
13.2 +++ b/src/Pure/Thy/thy_output.ML Tue May 03 22:27:32 2011 +0200
13.3 @@ -450,9 +450,9 @@
13.4 val _ = add_option "show_structs" (Config.put show_structs o boolean);
13.5 val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
13.6 val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
13.7 -val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean);
13.8 -val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
13.9 -val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
13.10 +val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
13.11 +val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
13.12 +val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
13.13 val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
13.14 val _ = add_option "display" (Config.put display o boolean);
13.15 val _ = add_option "break" (Config.put break o boolean);
14.1 --- a/src/Pure/Tools/find_theorems.ML Tue May 03 22:26:16 2011 +0200
14.2 +++ b/src/Pure/Tools/find_theorems.ML Tue May 03 22:27:32 2011 +0200
14.3 @@ -383,9 +383,9 @@
14.4 val shorten =
14.5 Name_Space.extern
14.6 (ctxt
14.7 - |> Config.put Name_Space.long_names false
14.8 - |> Config.put Name_Space.short_names false
14.9 - |> Config.put Name_Space.unique_names false) space;
14.10 + |> Config.put Name_Space.names_long false
14.11 + |> Config.put Name_Space.names_short false
14.12 + |> Config.put Name_Space.names_unique false) space;
14.13
14.14 fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
14.15 nicer_name (shorten x, i) (shorten y, j)