# HG changeset patch # User wenzelm # Date 1304454452 -7200 # Node ID 04dfffda56712ade590891db12b456c187c824b6 # Parent b98f22593f971e4fd1999e74b98532405ac92cef more conventional naming scheme: names_long, names_short, names_unique; diff -r b98f22593f97 -r 04dfffda5671 NEWS --- 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 diff -r b98f22593f97 -r 04dfffda5671 doc-src/Codegen/Thy/Setup.thy --- 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 diff -r b98f22593f97 -r 04dfffda5671 doc-src/IsarRef/Thy/Document_Preparation.thy --- 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. diff -r b98f22593f97 -r 04dfffda5671 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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. diff -r b98f22593f97 -r 04dfffda5671 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- 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. diff -r b98f22593f97 -r 04dfffda5671 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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. diff -r b98f22593f97 -r 04dfffda5671 doc-src/LaTeXsugar/Sugar/Sugar.thy --- 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. *} diff -r b98f22593f97 -r 04dfffda5671 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- 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% diff -r b98f22593f97 -r 04dfffda5671 doc-src/TutorialI/Misc/Itrev.thy --- 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 (*>*) diff -r b98f22593f97 -r 04dfffda5671 src/Pure/General/name_space.ML --- 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; diff -r b98f22593f97 -r 04dfffda5671 src/Pure/Isar/attrib.ML --- 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 #> diff -r b98f22593f97 -r 04dfffda5671 src/Pure/ProofGeneral/preferences.ML --- 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 diff -r b98f22593f97 -r 04dfffda5671 src/Pure/Thy/thy_output.ML --- 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); diff -r b98f22593f97 -r 04dfffda5671 src/Pure/Tools/find_theorems.ML --- 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)