| Mon, 31 Dec 2012 20:30:03 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 18:23:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 20:05:53 +0100 |
wenzelm |
prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:46:33 +0100 |
wenzelm |
include command results in tooltip as well;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2012 19:51:43 +0100 |
wenzelm |
updated to jedit-5.0.0;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:22:29 +0100 |
wenzelm |
reset active areas on content update;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 11:42:16 +0100 |
wenzelm |
always reset active areas;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 14:53:02 +0100 |
wenzelm |
reset active area for outdated snapshot (again?);
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 14:40:39 +0100 |
wenzelm |
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 21:52:45 +0200 |
wenzelm |
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 23:38:48 +0200 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:40:35 +0200 |
wenzelm |
use Pretty_Tooltip for Graphview_Panel;
|
file |
diff |
annotate
|
| 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
|