Re: [isabelle] Another newbie question...case-based proofs



Hi

> In general, I’d appreciate it a lot if the Isabelle IDE could be made
> more comfortable for people who mostly use the keyboard and can get
> on
> speed with it. In particular, it would be great if the completion
> mechanism could be improved.

You can set "completion delay" to 0 in the options ... that's one of
the first things I do when I set up a new Isabelle version! The upside
is that hardcoded completions (eg unicode symbols) come up immediately.
The downside is that dynamic completions (eg lemma names) that come
from Isabelle through PIDE are not yet there ... you'll have to press
CTRL-B (or whatever shortcut you have for auto-completion), to also
make these completions appear.


> Another problem with the completion mechanism is that a completion
> list
> sometimes pops up when you don’t need it (typically after entering a
> quotation mark), and then you cannot navigate the cursor up or down.

I think you can configure this in etc/symbols. The one on quotation
marks was introduced to remember the user that cartouches should be
used where possible, instead of quots.


--
  Peter






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