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

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 MHonArc.