hide: added option '(open)';

--- a/NEWS	Wed Sep 14 23:14:59 2005 +0200
+++ b/NEWS	Wed Sep 14 23:15:00 2005 +0200
@@ -223,6 +223,8 @@
 wrt. the last state (works for interactive theory development only),
 in proof mode print all local facts (cf. 'print_facts');
 
+* 'hide': option '(open)' hides only base names.
+
 * More efficient treatment of intermediate checkpoints in interactive
 theory development.
 

--- a/doc-src/IsarRef/pure.tex	Wed Sep 14 23:14:59 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed Sep 14 23:15:00 2005 +0200
@@ -399,7 +399,7 @@
 \end{matharray}
 
 \begin{rail}
-  'hide' name (nameref + )
+  'hide' ('(' 'open' ')')? name (nameref + )
   ;
 \end{rail}
 
@@ -418,11 +418,15 @@
   Note that global names are prone to get hidden accidently later, when
   qualified names of the same base name are introduced.
   
-\item [$\isarkeyword{hide}~space~names$] removes declarations from a given
-  name space (which may be $class$, $type$, or $const$).  Hidden objects
-  remain valid within the logic, but are inaccessible from user input.  In
-  output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
-  full internal name.  Unqualified (global) names may not be hidden.
+\item [$\isarkeyword{hide}~space~names$] fully removes declarations from a
+  given name space (which may be $class$, $type$, or $const$); with the
+  $(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 ``$\mathord?\mathord?$''
+  prefixed to the full internal name.
 \end{descr}
 
 

--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 14 23:14:59 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 14 23:15:00 2005 +0200
@@ -223,7 +223,8 @@
 
 val hideP =
   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
-    (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o Sign.hide_names true));
+    ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
+      (Toplevel.theory o uncurry Sign.hide_names));
 
 
 (* use ML text *)