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

... if the definition is in a separate file.

2012/12/17 Fabian Immler <immler at>:
> 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.