| Sun, 18 Nov 2012 14:24:30 +0100 |
wenzelm |
more accurate pixel_range -- do not round offset here;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 13:52:54 +0100 |
wenzelm |
tuned signature;
|
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
|
| 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
|
| Mon, 17 Sep 2012 18:14:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 18:06:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:56:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:49:11 +0200 |
wenzelm |
somewhat more general JEdit_Lib;
|
file |
diff |
annotate
|