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



Hi Holger,

I find that if you ctrl+click on a function name, then the focus jumps to the definition of that function.

John

On 17 Dec 2012, at 16:58, Holger Blasum wrote:

> Dear all,
> 
> I would ask that when you ctrl+hover on a function definition 
> (such as mysucc in attached hover.thy) then not only the 
> typing information of mysucc ("nat => nat") shows up but 
> also the body of the function ("mysucc n = n + 1"). Or does that 
> feature already exist?
> 
> best,
> 
> -- 
> Holger
> <hover.thy>






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