Re: [isabelle] Feature request: definition on crtl+hover

Hello Makarius,

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
> connected.
> 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.

Happy 2013,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.