Re: [isabelle] Feature request: definition on crtl+hover

There is also jEdits command "Go to recent buffer" with its predefined
shortcut Ctrl-`.

2012/12/17 Lars Noschinski <noschinl at>:
> On 17.12.2012 17:45, Holger Blasum wrote:
>> Also, if I understand correctly (again, maybe I
>> miss sth) when I use Ctrl+Click on a function name then there is no
>> single-key way back (like pressing "Esc" or something ...) to where
>> the focus was before.
> You could try playing around with the Navigator extension.

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