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

Tjark Weber webertj at in.tum.de
Mon Aug 13 14:50:18 CEST 2012


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,

Ceterum censeo: Isabelle needs an issue tracker.

More information about the isabelle-dev mailing list