Stacking of tooltips is nice. Also that these stay "open" until they are
closed explicitly is far more convenient than the previous behavior. A
tiny remark: for linux (and I guess also windows) users, it is
surprising to have icons on the top-left of a "window", rather than
top-right :D. I'm just saying.
cheers
chris
On 10/05/2012 11:40 PM, Makarius wrote:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
