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



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.