Re: [isabelle] Feature request: definition on crtl+hover
Try using Markers.
I just wish that they worked between files, and not just within a single file.
On 17 Dec 2012, at 16:45, Holger Blasum <hbl at sysgo.com> wrote:
> Hi John,
> On 12-17, John Wickerson wrote:
>> I find that if you ctrl+click on a function name, then the focus jumps to the definition of that function.
> Ctrl+Click is certainly useful and well-intentioned. But I feel jumping
> with the focus disrupts workflow more than it would just show up as
> tool tip (by Ctrl+hover). 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and