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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
