Thu, 04 Oct 2012 20:14:40 +0200 |
wenzelm |
separate module Pretty_Tooltip;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 19:31:50 +0200 |
wenzelm |
refined rich tooltip options;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 18:28:31 +0200 |
wenzelm |
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
|
file |
diff |
annotate
|
Fri, 21 Sep 2012 16:50:44 +0200 |
wenzelm |
more realistic sendback: pick exec_id from message position and text from buffer;
|
file |
diff |
annotate
|
Fri, 21 Sep 2012 15:39:51 +0200 |
wenzelm |
some support for hovering and sendback area;
|
file |
diff |
annotate
|
Thu, 20 Sep 2012 22:25:30 +0200 |
wenzelm |
tuned painter;
|
file |
diff |
annotate
|
Thu, 20 Sep 2012 21:31:56 +0200 |
wenzelm |
tuned rendering;
|
file |
diff |
annotate
|
Wed, 19 Sep 2012 12:10:40 +0200 |
wenzelm |
more robust GUI component handlers;
|
file |
diff |
annotate
|
Mon, 17 Sep 2012 20:34:19 +0200 |
wenzelm |
renamed Text_Area_Painter to Rich_Text_Area;
|
file |
diff |
annotate
| base
|