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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev