Re: [isabelle] Tab completion slow in Isabelle2014-RC2
Am 08.08.14 12:22, schrieb Makarius:
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
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).
Thanks that helped.
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.
Sounds nice. But I'd like to have the "old" context insensitive
completions (at least the first one) at the default and the possibility
to always select it immediately. Maybe the completion list should be
updated with additional completions that take more time.
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.
Have you tried setting up the sledgehammer panel on a regular 1080p
display? There's just not enough vertical space to have the editor, the
output and the Sledgehammer panel for my taste. Switching views or using
the mouse is not an option for me. Also I'd like some marker in the text
showing me "here is some sledgehammer instance running click me to get
to the results".
This archive was generated by a fusion of
Pipermail (Mailman edition) and