--- a/NEWS Fri Apr 16 21:28:09 2010 +0200
+++ b/NEWS Fri Apr 16 22:15:09 2010 +0200
@@ -71,6 +71,10 @@
in subsequent goal refinement steps. Tracing may also still be
enabled or disabled via the ProofGeneral settings menu.
+* Separate commands 'hide_class', 'hide_type', 'hide_const',
+'hide_fact' replace the former 'hide' KIND command. Minor
+INCOMPATIBILITY.
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/Spec.thy Fri Apr 16 21:28:09 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri Apr 16 22:15:09 2010 +0200
@@ -1225,11 +1225,14 @@
\begin{matharray}{rcl}
@{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
- 'hide' ('(open)')? name (nameref + )
+ ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
;
\end{rail}
@@ -1251,17 +1254,20 @@
Note that global names are prone to get hidden accidently later,
when qualified names of the same base name are introduced.
- \item @{command "hide"}~@{text "space names"} fully removes
- declarations from a given name space (which may be @{text "class"},
- @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
- "(open)"} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
+ \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
+ may never be hidden.
+
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no
longer accessible to the user are printed with the special qualifier
``@{text "??"}'' prefixed to the full internal name.
+ \item @{command "hide_type"}, @{command "hide_const"}, and @{command
+ "hide_fact"} are similar to @{command "hide_class"}, but hide types,
+ constants, and facts, respectively.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Apr 16 21:28:09 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Apr 16 22:15:09 2010 +0200
@@ -1268,11 +1268,14 @@
\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}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \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}} \\
+ \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\end{matharray}
\begin{rail}
- 'hide' ('(open)')? name (nameref + )
+ ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
;
\end{rail}
@@ -1292,16 +1295,19 @@
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}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
- declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
- \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
+ \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
+ may never be hidden.
+
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no
longer accessible to the user are printed with the special qualifier
``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
+ \item \hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}, \hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}, and \hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}} are similar to \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}, but hide types,
+ constants, and facts, respectively.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%