Re: [isabelle] Isabelle2014-RC4: Isabelle/jEdit action for C-hover

Christian Sternagel wrote:
> Is there already an action (or command, I'm not sure on the naming here) in
> Isabelle/jEdit for whatever C-hover does internally. Then a keyboard
> shortcut could be assigned to it, avoiding the need to use the mouse.

I'd like to add to this, because I've been one of the people to bother
Chris with this question.

I'm not a strong opponent of using the mouse, though I think that having
keyboard shortcuts for common actions is very desirable for efficiency,
and looking up types of identifiers is a very common interaction when
using Isabelle, so deserves having such a shortcut. (Note that the
cursor will often be in the vicinity of the identifier of interest,
while the mouse pointer may be anywhere in the jedit window.)

Despite having no issues with using the mouse per se, I find C-hover
very annoying. There are two reasons for this with Isabelle/jedit's
default settings. The more important one is that my usual approach for
mouse interaction is to move the mouse to the right spot, and then click
appropriately. With C-hover, one has to press the Control key before the
mouse pointer comes to rest; if I forget doing that, I have to press
Control and wiggle with the mouse; rather than one interaction with the
mouse I now need two. The second issue I'm experiencing is that the
popup does not appear immediately, i.e. the UI forces me to wait.
Fortunately, one can reduce the popup delay to improve interactivity.



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