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 http://sourceforge.net/projects/jedit/

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 feature request.

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.

Regards,
GB






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.