[isabelle-dev] Notes on datatype_new list

[Makarius]

On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:

>> (3) A genuine name space problem: "list" is concealed, and thus cannot 
>> be completed in semantic completion.
>
> I presume you are referring to the fact that
>
>    @{const_name Cons} = "List.list.Cons"
>    @{const_name hd} = "List.list.hd"
>    @{const_name map} = "List.list.map"
>    @{const_name rec_list} = "List.list.rec_list"
>
> where the "list" component is optional. This behavior is deliberate -- 
> this is what the old package did with all the constants it defined. In 
> other words,

> The only novelty is that we followed the same idiom for the other 
> constants introduced by the package, such as "hd" and "map".

(This is the easy part of this thread.)

I fully agree with this uniform additional qualification -- it is mainly 
for internal robustness.


The observed here problem is different: the type constructor "list" 
somehow ends up in the name space with a "concealed" flag.  There might be 
one or more Binding.conceal too many in the BNF sources.


I should probably issue some warning or special PIDE markup whenever a 
plain name given in user space is resolved to some concealed entity.


 	Makarius