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


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?


	Makarius





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