[isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click

[Christian Sternagel]

I would also regard all of the below suggestions as rather convenient (I 
wanted to asked for 1 and 4 myself already several times, but somehow 
never got around). - cheers chris

On 08/13/2012 09:50 PM, Tjark Weber wrote:
> Hi,
>
> Ctrl-click in Isabelle/jEdit "exposes additional information" - about
> the next best thing since sliced bread. I have a few suggestions for
> related features that would be nice to have, in my opinion (provided
> they are not too much implementation work):
>
> 1) In "theory T imports A", I'd like to be able to Ctrl-click on A to
> open the corresponding theory file.
>
> 2) In "use filename", I'd like to be able to Ctrl-click on "filename" to
> open the corresponding file.
>
> 3) In "ML {* open Foo; *}", I'd like to be able to Ctrl-click on Foo to
> see its definition.
>
> 4) Ctrl-click on an ML identifier takes me to its declaration (typically
> in some signature). Wouldn't it be more useful to be taken to its
> definition (i.e., the actual implementation, typically in a structure)?
>
> Best regards,
> Tjark
>