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