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 in.tum.de>:
> 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.