[isabelle-dev] jEdit: <ctrl> + <click> trouble

[Steffen Juilf Smolka]

Hi,

there is a little annoying inconvenience with the <ctrl> + <click> shortcut for jumping to definitions in jEdit.
To click an element, one oviously has to point at the element first.
When waiting for too long before clicking, the <ctrl> + <hover> shortcut will fire an bring up a popup - unfortunately, at this point,<ctrl> + <click> will no longer work, probably because the focus is no longer on the element pointed at, but at the popup.

So, in essance, for the <ctrl> + <click> shortcut to work, one has to beat the popup delay.
Not knowing this can cause quite some frustration.

I posted this here rather than on the bitbucket site for the release since I think this is more an imperfection than a bug, and I don't know if it is importan enough to be considered before the release.

I'm running MacOS Mountain Lion and Isabelle aafd4270b4d4

Regards,
Steffen