doc-src/IsarRef/Thy/document/Spec.tex
changeset 36177 8e0770d2e499
parent 35681 8b22a498b034
child 36178 0e5c133b48b6
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 21:28:09 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:15:09 2010 +0200
     1.3 @@ -1268,11 +1268,14 @@
     1.4  \begin{matharray}{rcl}
     1.5      \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.6      \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.7 -    \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.8 +    \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.9 +    \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.10 +    \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.11 +    \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.12    \end{matharray}
    1.13  
    1.14    \begin{rail}
    1.15 -    'hide' ('(open)')? name (nameref + )
    1.16 +    ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
    1.17      ;
    1.18    \end{rail}
    1.19  
    1.20 @@ -1292,16 +1295,19 @@
    1.21    Note that global names are prone to get hidden accidently later,
    1.22    when qualified names of the same base name are introduced.
    1.23    
    1.24 -  \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
    1.25 -  declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
    1.26 -  \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
    1.27 -  (unqualified) names may never be hidden.
    1.28 -  
    1.29 +  \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
    1.30 +  declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
    1.31 +  option, only the base name is hidden.  Global (unqualified) names
    1.32 +  may never be hidden.
    1.33 +
    1.34    Note that hiding name space accesses has no impact on logical
    1.35    declarations --- they remain valid internally.  Entities that are no
    1.36    longer accessible to the user are printed with the special qualifier
    1.37    ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
    1.38  
    1.39 +  \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,
    1.40 +  constants, and facts, respectively.
    1.41 +  
    1.42    \end{description}%
    1.43  \end{isamarkuptext}%
    1.44  \isamarkuptrue%