[isabelle-dev] NEWS: more informative errors in lazy enumerations

[Makarius]

On Tue, 20 Nov 2012, Peter Lammich wrote:

> Wouldn't it be better to just enumerate "censored" completions always 
> last in the completion list? Or are there technical difficulties to do 
> so?

There is no technical difficulty, but it would be yet another feature. 
Every feature is a burden, first to implement it, and then doubly-so in 
the long-term maintenance.  (I spend most of my time on the latter these 
days.)

I have many more things on my list to improve the completion mechanism, 
before such a detail would be considered again.


 	Makarius