Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
Am 27/08/2012 13:35, schrieb Makarius: 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. Just for the record: I have spent over 20k EUR to this over the past 1 1/2 years but that will have to be it from the TUM side. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
Various projects of mine, going back many years, have supported Poly/ML at the rate of £1000 per year. (That's just under €1300.) This is a much better use of grant money than to give it to already wealthy publishers for the sake of so-called Gold open access. Larry On 27 Aug 2012, at 16:18, Tobias Nipkow nip...@in.tum.de wrote: Just for the record: I have spent over 20k EUR to this over the past 1 1/2 years but that will have to be it from the TUM side. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
On Mon, 2012-08-27 at 13:35 +0200, Makarius 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. Nice. I suspect it would be considerably more work to support C-click in already loaded theories (e.g., HOL/Main)? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
