[isabelle-dev] NEWS: limited name space accesses

[Makarius]

On Tue, 7 Apr 2015, Tobias Nipkow wrote:

>
> On 07/04/2015 14:37, Christian Sternagel wrote:
>>    (b) qualified
>
> That gets my vote because it expresses clearly the description Makarius 
> gave: "name space entry that is only accessible by qualified names"

It is definitely good to collect keyword candidates from other well-known 
languages.

I had "qualified" on my list of possibilities at first, but was hesitating 
to use it, because there is yet another concept (c) that has no Isar 
notation so far.  It is called Binding.qualified in ML and could solve 
problems like 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html 
as follows:

   locale test
   begin

     lemma foo (qualified bar!): ...

   end


In principle there could be a dual-use of 'qualified' as Binding.qualified 
(with argument) and Name_Space.restricted (without argument), or rather 
Name_Space.qualified after another "tuned signature" change.

   qualified lemma a: ...

   lemma b (qualified c): ...
   lemma e (qualified f!): ...

This does not work in outer syntax though, since the new command prefix 
category (keywords that may occur before a command) needs to be disjoint 
from other minor keywords in the command body.  (After the dismissal of 
Proof General, command spans have become a bit more flexible, but cannot 
be stretched arbitrarily.)


One could try to invent another notation for "x (qualified y!)" above. 
Note that the "!" is the mandatory flag (like in locale interpretation 
syntax).  We don't have notation for such flags within qualified names 
themselves.  Otherwise one could use "c.b" directly.

A real danger in the whole affair is that we need to proceed towards the 
Isabelle2015 release very soon, i.e. this week.


As a summary, here is the collection of nice keywords so far, without any 
assignment of meanings yet:

   private
   local
   hidden
   qualified

Anything else?


 	Makarius