Re: [isabelle] Feature request: definition on crtl+hover
- To: Makarius <makarius at sketis.net>
- Subject: Re: [isabelle] Feature request: definition on crtl+hover
- From: Holger Blasum <hbl at sysgo.com>
- Date: Wed, 2 Jan 2013 09:25:01 +0100
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <alpine.LNX.email@example.com>
- 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>
- User-agent: Mutt/1.5.21 (2010-09-15)
On 12-22, Makarius wrote:
> On Tue, 18 Dec 2012, Holger Blasum wrote:
> >You're right what is interesting is the definition as defined by
> >the user, not the one internally seen by Isabelle (iirc debuggers
> >also do it this way). Does Isabelle internally only keep track of
> >where the definition begins (theory file, offset within the theory
> >file) or also where it ends? (The latter would allow cutting the
> >text ...)
> 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 ...").
> >Further inspection revealed that inserting "Style jEdit*
> >SloppyFocus" also fixes the disappearing jEdit subwindow for my
> >configuration (without having to use SloppyFocus elsewhere).
> I will look at this again myself. Someone else has reported focus
> inversion problems with the latest Unity/Compiz of Ubuntu 12.10, so
> this might be more than just an incident of vintage window managers.
Thanks for properly fixing this. That is, fvwm-wise, it now works not
only with fvwm SloppyFocus pointer focus model, but also with the fvwm
FocusFollowsMouse pointer focus model.
This archive was generated by a fusion of
Pipermail (Mailman edition) and