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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
