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

Hi Makarius,

On 12-17, Makarius wrote:
> Another idea in the pipeline is to improve the content and
> flexibility of the Isabelle/jEdit popup window: it could show you
> the part of the relevant source outright, or some documentation.

That was I what I had asked for. To understand it: is the definition
of a function (or an abbreviation, another use case, this is the one
I was originally asked when showing a theory with abbreviations to
a coworker, where typing information "bool" wasn't really informative) 
less "available" at run-time than its typing information?

> The next release will already have a popup that is recursively again
> a jEdit text area at a small scale, but without the extra
> functionality sketched here.

I've noticed this - being positively surprised how smoothly the stuff just
randomly plucked from the repository today compiles and works :-)
Only that I haven't figured out yet how to enter the window without
it disappearing from (a possibly non-standard-configured) fvwm, but 
it works in xfce4. But anyway, the tool tip's presentation is orthogonal 
to its content (and I think the former is more important).



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