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> 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. 
> Best,
> -- 
> Holger

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.