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

[Makarius]

On Mon, 27 Aug 2012, Christian Sternagel wrote:

>> 1) In "theory T imports A", I'd like to be able to Ctrl-click on A to
>> open the corresponding theory file.

See some changesets leading up to Isabelle/10b89c127153 how I've spent 
Sunday afternoon.


>> 2) In "use filename", I'd like to be able to Ctrl-click on "filename" to
>> open the corresponding file.

This works for the new 'ML_file' command.  Old 'uses' / 'use' will 
probably disappear soon -- I am still working on some details there.


I also want to emphasize again that "using" the repository version is not 
the way to get the "lastest features" earlier that everybody else.  It 
rather means that you somehow participate in the ongoing construction 
process in what will become a proper release eventually.

So it is important to point out omissions or snags, but without any 
expectation that it is addressed in real-time.  You also need to be ready 
to work with half-finished things until the next release.


>> 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)?

Poly/ML is responsible for providing markup here.  What works now works 
because someone managed to get a little bit of funding organized and 
directed towards David Matthews some years ago.

It is generally a good move to develop a habit to allocate some small 
amounts in project proposals etc. for "Poly/ML software maintenance" and 
direct it to David.  This is how things can continue, and David gets a 
tiny little bit of recompense for his amazing work on the system.


 	Makarius