discontinued obsolete 'global' and 'local' commands;
authorwenzelm
Wed Aug 25 14:18:09 2010 +0200 (2010-08-25)
changeset 387088915e3ce8655
parent 38707 d81f4d84ce3b
child 38709 04414091f3b5
discontinued obsolete 'global' and 'local' commands;
NEWS
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/HOL/HOL.thy
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Wed Aug 25 11:30:45 2010 +0200
     1.2 +++ b/NEWS	Wed Aug 25 14:18:09 2010 +0200
     1.3 @@ -32,6 +32,11 @@
     1.4  * Diagnostic command 'print_interps' prints interpretations in proofs
     1.5  in addition to interpretations in theories.
     1.6  
     1.7 +* Discontinued obsolete 'global' and 'local' commands to manipulate
     1.8 +the theory name space.  Rare INCOMPATIBILITY.  The ML functions
     1.9 +Sign.root_path and Sign.local_path may be applied directly where this
    1.10 +feature is still required for historical reasons.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 25 11:30:45 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 25 14:18:09 2010 +0200
     2.3 @@ -1220,8 +1220,6 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 -    @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
     2.9      @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
    2.10      @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
    2.11      @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
    2.12 @@ -1241,16 +1239,6 @@
    2.13  
    2.14    \begin{description}
    2.15  
    2.16 -  \item @{command "global"} and @{command "local"} change the current
    2.17 -  name declaration mode.  Initially, theories start in @{command
    2.18 -  "local"} mode, causing all names to be automatically qualified by
    2.19 -  the theory name.  Changing this to @{command "global"} causes all
    2.20 -  names to be declared without the theory prefix, until @{command
    2.21 -  "local"} is declared again.
    2.22 -  
    2.23 -  Note that global names are prone to get hidden accidently later,
    2.24 -  when qualified names of the same base name are introduced.
    2.25 -  
    2.26    \item @{command "hide_class"}~@{text names} fully removes class
    2.27    declarations from a given name space; with the @{text "(open)"}
    2.28    option, only the base name is hidden.  Global (unqualified) names
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 11:30:45 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 14:18:09 2010 +0200
     3.3 @@ -1262,8 +1262,6 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{matharray}{rcl}
     3.7 -    \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.8 -    \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.9      \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    3.10      \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    3.11      \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    3.12 @@ -1283,14 +1281,6 @@
    3.13  
    3.14    \begin{description}
    3.15  
    3.16 -  \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
    3.17 -  name declaration mode.  Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
    3.18 -  the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
    3.19 -  names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
    3.20 -  
    3.21 -  Note that global names are prone to get hidden accidently later,
    3.22 -  when qualified names of the same base name are introduced.
    3.23 -  
    3.24    \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
    3.25    declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
    3.26    option, only the base name is hidden.  Global (unqualified) names
     4.1 --- a/etc/isar-keywords-ZF.el	Wed Aug 25 11:30:45 2010 +0200
     4.2 +++ b/etc/isar-keywords-ZF.el	Wed Aug 25 14:18:09 2010 +0200
     4.3 @@ -73,7 +73,6 @@
     4.4      "fix"
     4.5      "from"
     4.6      "full_prf"
     4.7 -    "global"
     4.8      "guess"
     4.9      "have"
    4.10      "header"
    4.11 @@ -97,7 +96,6 @@
    4.12      "lemmas"
    4.13      "let"
    4.14      "linear_undo"
    4.15 -    "local"
    4.16      "local_setup"
    4.17      "locale"
    4.18      "method_setup"
    4.19 @@ -369,7 +367,6 @@
    4.20      "extract"
    4.21      "extract_type"
    4.22      "finalconsts"
    4.23 -    "global"
    4.24      "hide_class"
    4.25      "hide_const"
    4.26      "hide_fact"
    4.27 @@ -378,7 +375,6 @@
    4.28      "instantiation"
    4.29      "judgment"
    4.30      "lemmas"
    4.31 -    "local"
    4.32      "local_setup"
    4.33      "locale"
    4.34      "method_setup"
     5.1 --- a/etc/isar-keywords.el	Wed Aug 25 11:30:45 2010 +0200
     5.2 +++ b/etc/isar-keywords.el	Wed Aug 25 14:18:09 2010 +0200
     5.3 @@ -102,7 +102,6 @@
     5.4      "full_prf"
     5.5      "fun"
     5.6      "function"
     5.7 -    "global"
     5.8      "guess"
     5.9      "have"
    5.10      "header"
    5.11 @@ -128,7 +127,6 @@
    5.12      "lemmas"
    5.13      "let"
    5.14      "linear_undo"
    5.15 -    "local"
    5.16      "local_setup"
    5.17      "locale"
    5.18      "method_setup"
    5.19 @@ -469,7 +467,6 @@
    5.20      "fixpat"
    5.21      "fixrec"
    5.22      "fun"
    5.23 -    "global"
    5.24      "hide_class"
    5.25      "hide_const"
    5.26      "hide_fact"
    5.27 @@ -479,7 +476,6 @@
    5.28      "instantiation"
    5.29      "judgment"
    5.30      "lemmas"
    5.31 -    "local"
    5.32      "local_setup"
    5.33      "locale"
    5.34      "method_setup"
     6.1 --- a/src/HOL/HOL.thy	Wed Aug 25 11:30:45 2010 +0200
     6.2 +++ b/src/HOL/HOL.thy	Wed Aug 25 14:18:09 2010 +0200
     6.3 @@ -57,14 +57,18 @@
     6.4    False         :: bool
     6.5    Not           :: "bool => bool"                   ("~ _" [40] 40)
     6.6  
     6.7 -global consts
     6.8 +setup Sign.root_path
     6.9 +
    6.10 +consts
    6.11    "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
    6.12    "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
    6.13    "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
    6.14  
    6.15    "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
    6.16  
    6.17 -local consts
    6.18 +setup Sign.local_path
    6.19 +
    6.20 +consts
    6.21    The           :: "('a => bool) => 'a"
    6.22    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    6.23    Ex            :: "('a => bool) => bool"           (binder "EX " 10)
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 25 11:30:45 2010 +0200
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 25 14:18:09 2010 +0200
     7.3 @@ -286,14 +286,6 @@
     7.4  
     7.5  (* name space entry path *)
     7.6  
     7.7 -val _ =
     7.8 -  Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
     7.9 -    (Scan.succeed (Toplevel.theory Sign.root_path));
    7.10 -
    7.11 -val _ =
    7.12 -  Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
    7.13 -    (Scan.succeed (Toplevel.theory Sign.local_path));
    7.14 -
    7.15  fun hide_names name hide what =
    7.16    Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
    7.17      ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>