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

Hi Makarius,

On 12-17, Makarius wrote:
> First one needs to think about the canonical "definition" you want
> to see, which is not necessarily the actual logical definition.  I
> did not engage it that seriously so far, simply because it was too
> far off.
> There is also the question about volume of formal document content
> emitted by the prover towards the front-end.  Types (and sorts in
> the coming release) still work, but flooding with all possible term
> expansions by default will pose problems.  It might have to be done
> more lazily, or on explicit request, but this is still
> underdeveloped.
> The sources where you define things in a certain external form are
> better suited.  No additional volume produced by the prover -- they
> are already there -- and no question how to present them -- you did
> it already yourself.

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

> Works usually means "works for me" in a restricted sense.  There are
> still many issues pending for the coming release, and we are already
> in the consolidation phase.  To continue the "use of latest
> repository game" seriously, you have to subscribe to the
> isabelle-dev mailing list, for two-way information exchange: you
> need to know about recent moves, and we need to get feedback about
> open problems.  The repository is no magic door to get the latest
> features earlier than others, it rather means you have time to spend
> to work out issues you encounter.

Understood. In this case I was simply once-only checking whether
the feature I was looking for perhaps was already implemented in
head, and for that I was happy to get the thing started at all ... 
Cannot claim serious commitment to bleeding edge per se.

> You surely have your own strange fvwm configuration.
> Wasn't that fvwm2 back then in 1995?  Or do you have fvwm95 with the
> Windows 95 retro look?

Checked this (should have done so before), it was really just my
configuration, e.g. works fine with fvwm default configuration when
wheezy debian package is just installed without fiddling. Further
inspection revealed that inserting "Style jEdit* SloppyFocus" also fixes 
the disappearing jEdit subwindow for my configuration (without having to use 
SloppyFocus elsewhere). I also begin to see the usefulness of 
the new-window feature because it allows (combined with above request for 
putting meaningful text into it) that definitions or abbreviations could
be unfolded step-by-step to arbitrary depth by the user.



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