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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
