On Sat, 25 Jun 2011, Lawrence Paulson wrote:
Is it possible to restrict command completion to a select collection of
commonly used commands? Or to make it the user-configurable? Larry
On 24 Jun 2011, at 21:01, Alexander Krauss wrote:
Suggestion: Simply kill completion of commands (not symbols)???
In principle everything is possible, but one needs to try hard to minimize
"options" and "features". Otherwise it becomes impossible to maintain
robustness of the application. There are no proper automated test
procedures, which means I usually play through all the important things
manually (on 3 platform families).
I have already spent a lot of time looking through the existing mechanisms
of Java, Swing, jEdit, and make as much sense of it as is feasible at the
moment. This needs to continue, of course.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
