Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
file |
diff |
annotate
|
Thu, 22 Nov 2012 17:11:26 +0100 |
wenzelm |
pack window before accessing its geometry;
|
file |
diff |
annotate
|
Thu, 22 Nov 2012 16:55:53 +0100 |
wenzelm |
more precise tooltip window size;
|
file |
diff |
annotate
|
Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 13 Oct 2012 00:08:36 +0200 |
wenzelm |
improved adhoc height for small fonts;
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 22:53:20 +0200 |
wenzelm |
more uniform tooltip color;
|
file |
diff |
annotate
|
Mon, 08 Oct 2012 12:40:35 +0200 |
wenzelm |
use Pretty_Tooltip for Graphview_Panel;
|
file |
diff |
annotate
|
Sun, 07 Oct 2012 16:26:31 +0200 |
wenzelm |
close tooltips more thoroughly;
|
file |
diff |
annotate
|
Sun, 07 Oct 2012 16:15:31 +0200 |
wenzelm |
make buttons closer to original mouse position;
|
file |
diff |
annotate
|
Sun, 07 Oct 2012 16:05:31 +0200 |
wenzelm |
detach tooltip as dockable window;
|
file |
diff |
annotate
|
Sun, 07 Oct 2012 15:05:11 +0200 |
wenzelm |
explicit close button;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 14:32:56 +0200 |
wenzelm |
further support for nested tooltips;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 13:48:22 +0200 |
wenzelm |
refer to parent frame -- relevant for floating dockables in particular;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 12:11:23 +0200 |
wenzelm |
tuned window position to fit on screen;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 12:00:28 +0200 |
wenzelm |
tuned window position;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 11:36:46 +0200 |
wenzelm |
determine window size from content;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 11:09:24 +0200 |
wenzelm |
tuned color and font size;
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 10:54:07 +0200 |
wenzelm |
close tooltip window on escape;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 20:36:10 +0200 |
wenzelm |
some re-ordering of initialization to ensure proper formatting;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 20:14:40 +0200 |
wenzelm |
separate module Pretty_Tooltip;
|
file |
diff |
annotate
|