# HG changeset patch # User wenzelm # Date 1282738689 -7200 # Node ID 8915e3ce8655f45135e9b70a226961a30e6215e0 # Parent d81f4d84ce3b98d293c7d85c953dff85d580c705 discontinued obsolete 'global' and 'local' commands; diff -r d81f4d84ce3b -r 8915e3ce8655 NEWS --- a/NEWS Wed Aug 25 11:30:45 2010 +0200 +++ b/NEWS Wed Aug 25 14:18:09 2010 +0200 @@ -32,6 +32,11 @@ * Diagnostic command 'print_interps' prints interpretations in proofs in addition to interpretations in theories. +* Discontinued obsolete 'global' and 'local' commands to manipulate +the theory name space. Rare INCOMPATIBILITY. The ML functions +Sign.root_path and Sign.local_path may be applied directly where this +feature is still required for historical reasons. + *** HOL *** diff -r d81f4d84ce3b -r 8915e3ce8655 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Wed Aug 25 11:30:45 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Aug 25 14:18:09 2010 +0200 @@ -1220,8 +1220,6 @@ text {* \begin{matharray}{rcl} - @{command_def "global"} & : & @{text "theory \ theory"} \\ - @{command_def "local"} & : & @{text "theory \ theory"} \\ @{command_def "hide_class"} & : & @{text "theory \ theory"} \\ @{command_def "hide_type"} & : & @{text "theory \ theory"} \\ @{command_def "hide_const"} & : & @{text "theory \ theory"} \\ @@ -1241,16 +1239,6 @@ \begin{description} - \item @{command "global"} and @{command "local"} change the current - name declaration mode. Initially, theories start in @{command - "local"} mode, causing all names to be automatically qualified by - the theory name. Changing this to @{command "global"} causes all - names to be declared without the theory prefix, until @{command - "local"} is declared again. - - Note that global names are prone to get hidden accidently later, - when qualified names of the same base name are introduced. - \item @{command "hide_class"}~@{text names} fully removes class declarations from a given name space; with the @{text "(open)"} option, only the base name is hidden. Global (unqualified) names diff -r d81f4d84ce3b -r 8915e3ce8655 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Aug 25 11:30:45 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Aug 25 14:18:09 2010 +0200 @@ -1262,8 +1262,6 @@ % \begin{isamarkuptext}% \begin{matharray}{rcl} - \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ @@ -1283,14 +1281,6 @@ \begin{description} - \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current - name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by - the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all - names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again. - - Note that global names are prone to get hidden accidently later, - when qualified names of the same base name are introduced. - \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global (unqualified) names diff -r d81f4d84ce3b -r 8915e3ce8655 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Wed Aug 25 11:30:45 2010 +0200 +++ b/etc/isar-keywords-ZF.el Wed Aug 25 14:18:09 2010 +0200 @@ -73,7 +73,6 @@ "fix" "from" "full_prf" - "global" "guess" "have" "header" @@ -97,7 +96,6 @@ "lemmas" "let" "linear_undo" - "local" "local_setup" "locale" "method_setup" @@ -369,7 +367,6 @@ "extract" "extract_type" "finalconsts" - "global" "hide_class" "hide_const" "hide_fact" @@ -378,7 +375,6 @@ "instantiation" "judgment" "lemmas" - "local" "local_setup" "locale" "method_setup" diff -r d81f4d84ce3b -r 8915e3ce8655 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Aug 25 11:30:45 2010 +0200 +++ b/etc/isar-keywords.el Wed Aug 25 14:18:09 2010 +0200 @@ -102,7 +102,6 @@ "full_prf" "fun" "function" - "global" "guess" "have" "header" @@ -128,7 +127,6 @@ "lemmas" "let" "linear_undo" - "local" "local_setup" "locale" "method_setup" @@ -469,7 +467,6 @@ "fixpat" "fixrec" "fun" - "global" "hide_class" "hide_const" "hide_fact" @@ -479,7 +476,6 @@ "instantiation" "judgment" "lemmas" - "local" "local_setup" "locale" "method_setup" diff -r d81f4d84ce3b -r 8915e3ce8655 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Aug 25 11:30:45 2010 +0200 +++ b/src/HOL/HOL.thy Wed Aug 25 14:18:09 2010 +0200 @@ -57,14 +57,18 @@ False :: bool Not :: "bool => bool" ("~ _" [40] 40) -global consts +setup Sign.root_path + +consts "op &" :: "[bool, bool] => bool" (infixr "&" 35) "op |" :: "[bool, bool] => bool" (infixr "|" 30) "op -->" :: "[bool, bool] => bool" (infixr "-->" 25) "op =" :: "['a, 'a] => bool" (infixl "=" 50) -local consts +setup Sign.local_path + +consts The :: "('a => bool) => 'a" All :: "('a => bool) => bool" (binder "ALL " 10) Ex :: "('a => bool) => bool" (binder "EX " 10) diff -r d81f4d84ce3b -r 8915e3ce8655 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Aug 25 11:30:45 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Aug 25 14:18:09 2010 +0200 @@ -286,14 +286,6 @@ (* name space entry path *) -val _ = - Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl - (Scan.succeed (Toplevel.theory Sign.root_path)); - -val _ = - Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl - (Scan.succeed (Toplevel.theory Sign.local_path)); - fun hide_names name hide what = Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>