Re: [isabelle] Line numbers vs. icons
On 12/2/2013 9:21 AM, Makarius wrote:
I have no problems to paint icons along-side the line numbers, if
jEdit provides free pixels for that.
You can try to convince the guys at
It might actually work out, since someone has enabled line numbers by
default in recent jEdit releases, but I reverted that for
Isabelle/jEdit to get the icons back.
To make a feature request, I would have to register with sourceforge,
and I try to be a part of as few Internet forums as possible. I would
make a feature request as a half-hearted demonstration to show that I do
my half-hearted part as a team player.
But, you would have to tell me that line numbers and icons can't already
coexist in the jEdit gutter, a statement I would include as part of a
In Eclipse, it appears there are two vertical areas which make up the
gutter, an area for graphical feedback, and an area for the line numbers.
In jEdit, there are two parts, an area for display of folding, and an
area which can only (apparently) show either line numbers, or graphical
information. There is the option "Global Options / Gutter / Selection
area width (in pixels)", but when line numbers are displayed, the option
"Minimal number of digits to reserve for line numbers" takes precedence,
and only line numbers are displayed. I don't know anything about it all
other than that.
I did a few searches on the Web looking for how to show both line
numbers and icons, but I didn't find anything.
This archive was generated by a fusion of
Pipermail (Mailman edition) and