[isabelle-dev] NEWS: limited name space accesses

[Makarius]

* Local theory specification commands may have a 'private' or
'restricted' modifier to limit name space accesses to the local scope,
as provided by some "context begin ... end" block. For example:

   context
   begin

   private definition ...
   private definition ...
   private lemma ...

   lemma ...
   lemma ...
   theorem ...

   end


This refers to Isabelle/83071f4c8ae6.

After more than 10 years in the pipeline, and never-ending efforts to 
localize almost all tools, there is now the long anticipated limitation of 
name space accesses. There are presently two example applications:

(1) Local tool setup with some auxiliary constants: "induct_forall" etc. 
in 
http://isabelle.in.tum.de/repos/isabelle/file/83071f4c8ae6/src/HOL/HOL.thy#l1377

(2) Plain specifications that are meant to produce theory-qualified names: 
AList.update etc. in 
http://isabelle.in.tum.de/repos/isabelle/file/e83ecf0a0ee1/src/HOL/Library/AList.thy#l11


I am still not 100% sure about the choice of keywords.  There are two 
concepts that are supported: (a) totally inaccessible name space entry, 
(b) name space entry that is only accessible by qualified names, not the 
base name.

Presently we have:

   (a) 'private'
   (b) 'restricted'

I first started out implementing 'private' for the sake of Eisbach, which 
really needs that.  Then I noticed that in practice one mostly uses 
'restricted' to eliminated old "hide (open)", but this keyword is a bit 
awkward.

Here are some possible alternatives:

   (a) 'hidden'    (like Long_Name.hidden according to Isabelle/ML terminology)
   (b) 'private'   (like 'private' in Java/Scala, in non-serious mode)

or:

   (a) 'private'   (like 'private' on Java/Scala in serious mode)
   (b) 'local'     (like an ancient Isabelle command of that name)


By non-serious mode I mean the rather easy way to bypass 'private' 
declarations on the JVM via reflection.  Likewise our logical environment 
always allows to access inaccessible names, after some tweaking of the 
name space, e.g. via aliases.  This could justify the use of 'private' for 
what is now 'restricted', or it might be just too confusing to users.


Note that it is now releatively easy to test feasibility of new keywords 
like this:

   $ isabelle build -n -a -d '$AFP' -k hidden -k local


 	Makarius