[isabelle-dev] jEdit: <ctrl> + <click> trouble
Steffen Juilf Smolka
steffen.smolka at in.tum.de
Tue Jan 22 16:33:33 CET 2013
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
More information about the isabelle-dev