Re: [isabelle] Feature request: definition on crtl+hover
On Mon, 17 Dec 2012, Holger Blasum wrote:
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?
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
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 :-)
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.
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).
It's not quite orthogonal. Having my own window popping up, allows to
define its content. I started experimenting with that already in 2010,
and then stopped after desparation with different Java look-and-feels,
platforms, window managers. In the version for the coming release, I
actually did try twm with spontaneous focus change and it worked. 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and