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



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

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