[isabelle-dev] Isabelle/jEdit output panel
makarius at sketis.net
Fri Oct 5 16:40:28 CEST 2012
On Fri, 21 Sep 2012, Makarius wrote:
> This also means that tooltips, hyperlinks etc. should now work the same
> for Output, just as for the input text.
> The next step will be to make tooltips and popups themselves use the
> same technology recursively.
The latter is now addressed in Isabelle/a1bd8fe5131b, which uses the new
Pretty_Tooltip everywhere for input or output. It also allows some
stacking of tooltips: activating the formal link in one tooltip opens
another. Thus a tooltip for type information can open another one for
sort information on the displayed type variables, for example.
Loss of focus or ESCAPE dispose such windows. Technically, this is a bit
like computer game programming: one needs to play with GUI events until it
works smoothly in the application. There are still some uneven situations
here, notably the keyboard focus.
More information about the isabelle-dev