Re: [isabelle] Feature request: definition on crtl+hover
There is also jEdits command "Go to recent buffer" with its predefined
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