[isabelle-dev] NEWS: more informative errors in lazy enumerations
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
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