Re: [isabelle] Feature request: definition on crtl+hover
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