Re: [isabelle] Feature request: definition on crtl+hover
- To: Holger Blasum <hbl at sysgo.com>
- Subject: Re: [isabelle] Feature request: definition on crtl+hover
- From: Makarius <makarius at sketis.net>
- Date: Thu, 3 Jan 2013 15:46:10 +0100 (CET)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <20130102082501.GA8502@hbl-lap-dell>
- References: <20121217155843.GA27471@hbl-lap-dell> <1DF69B41-F9AB-4B4A-ADD9-F5DF4FE841DA@cam.ac.uk> <20121217164526.GA30212@hbl-lap-dell> <50CF4D11.firstname.lastname@example.org> <CAHBFu05WSUeYzprw7eoA8i8zA8nLRnJQOHBNG_vG_e1A_2K40g@mail.gmail.com> <alpine.LNX.email@example.com> <20121217202513.GA6153@hbl-lap-dell> <alpine.LNX.firstname.lastname@example.org> <20121218071649.GA4810@hbl-lap-dell> <alpine.LNX.email@example.com> <20130102082501.GA8502@hbl-lap-dell>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Wed, 2 Jan 2013, Holger Blasum wrote:
On 12-22, Makarius wrote:
There is sufficient information to determine the full definition
range, lets say the language element like "fun ..." with all its
equations, or "function ..." with the following proof. For the
latter example there is a special case, though: there is a second
part following somewhere as "termination ..." which is not directly
Anything else should work smoothly, one the reference to sources is
wired up properly in the editor.
"Sufficient information to determine the full definition range"
sounds promising :-)
Why am I asking whether the end point information is available?
To my post of 17 Dec I attached a file hover.thy:
If we know that the definition of "mysucc" is in file hover.thy,
characters 0x49 to 0x5a, then it could perhaps be easy to implement
to display this information (that is, in this example, "mysucc n = n + 1")
once you ctrl+hover on mysucc (without having to jump through
the theories). From a usage perspective, I think
this could be very convenient, especially if one reads a theory
sb else has written ("what was this abbreviation she is using ...").
The "definition range" is the whole command span, starting with
"definition ..." and ending with "mysucc n = n + 1" in this example.
This is what I meant to show in the popup eventually.
In general, there is not just one equation defining a term, e.g. in "fun"
with several recursive equations, or several functions defined at the same
time. Showing the whole specification text should give sufficient clues
to the user. Lets see again how it looks when it is actually there (not
in the coming release.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and