wenzelm [Tue, 24 Nov 2015 22:50:03 +0100] rev 61746
paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
avoid hardwired colors (see 1d9c121cbe4d);
updated to Highlight 2.2;