[ jEdit-devel ] gutter updates

[mike d. <md...@st...>]

howdy-

i've been doing some jEdit work today on the Gutter, implementing the
current line highlighting that someone asked for and making things
generally nicer. hopefully, i sped some stuff up and reduced the amount of
unnecessary repainting, but it's quite possible i broke something. i guess
that's the reason we call these pre-release versions "devel".

i should have a diff ready soon. i'm still working on some font metrics
stuff.

-md