Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
Mon, 22 Oct 2012 16:27:55 +0200 |
wenzelm |
further attempts to cope with large files via option jedit_text_overview_limit;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 11:39:24 +0200 |
wenzelm |
option to bypass potentially slow text overview;
|
file |
diff |
annotate
|
Mon, 17 Sep 2012 20:34:19 +0200 |
wenzelm |
renamed Text_Area_Painter to Rich_Text_Area;
|
file |
diff |
annotate
|
Mon, 17 Sep 2012 20:23:25 +0200 |
wenzelm |
tuned signature -- more general Text_Area_Painter operations;
|
file |
diff |
annotate
|
Mon, 17 Sep 2012 17:49:11 +0200 |
wenzelm |
somewhat more general JEdit_Lib;
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 13:52:16 +0200 |
wenzelm |
more static handling of rendering options;
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 12:46:33 +0200 |
wenzelm |
tuned options (again);
|
file |
diff |
annotate
|
Thu, 13 Sep 2012 16:01:42 +0200 |
wenzelm |
more efficient painting based on cached result;
|
file |
diff |
annotate
|
Mon, 19 Mar 2012 23:08:27 +0100 |
wenzelm |
explicit propagation of assignment event, even if changed command set is empty;
|
file |
diff |
annotate
|
Tue, 21 Feb 2012 16:04:58 +0100 |
wenzelm |
separate module for text status overview;
|
file |
diff |
annotate
|