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

Makarius makarius at sketis.net
Tue Nov 20 15:24:22 CET 2012

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 

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


More information about the isabelle-dev mailing list