# HG changeset patch
# User wenzelm
# Date 1271448909 -7200
# Node ID 8e0770d2e49956c0b3c6608d1dbbcdefcabfd62c
# Parent  3fe7e97ccca8ae520f1df00226f468d4d8157a0a
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';

diff -r 3fe7e97ccca8 -r 8e0770d2e499 NEWS
--- 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 ***
 
diff -r 3fe7e97ccca8 -r 8e0770d2e499 doc-src/IsarRef/Thy/Spec.thy
--- 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}
 *}
 
diff -r 3fe7e97ccca8 -r 8e0770d2e499 doc-src/IsarRef/Thy/document/Spec.tex
--- 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%