[isabelle-dev] Isabelle/jEdit output panel

[Makarius]

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.


 	Makarius