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