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

[Tjark Weber]

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

-- 
Ceterum censeo: Isabelle needs an issue tracker.