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 to intermediate/0.
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.

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.
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.
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".

Best
    Benedikt





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.