Re: [isabelle] Tab completion slow in Isabelle2014-RC2
On Wed, 6 Aug 2014, bnord wrote:
When typing fast and using tab completion in Isabelle204-RC2 I often end
up with e.g. "sle<tab>" instead of "sledgehammer" when the system is
under some load. In 2013-2 no matter how hard I try I always get the
completion. I believe that I have changed all relevant settings to
You probably mean "immediate". I think you also need to switch off the
option "Completion Context" -- thus you are back to old-style syntactic
completion, independently of prover markup (which might get delayed and
thus cause non-determinism).
Instead of such a nostalgic mode that imitates old versions of
Isabelle/jEdit, I recommend to study the Isabelle/jEdit manual section
"3.5 Completion" and practice a little with the new defaults, which were
made for mixed syntactic / semantic completion.
To improve determinism on very light machines under load it might also
help to switch off the main "Completion" option and use the explicit key
sequence C+b instead.
For sledgehammer in particular, the canonical way is to use the
Sledgehammer panel instead of inserting a command.
This archive was generated by a fusion of
Pipermail (Mailman edition) and