18 Oct
2004
18 Oct
'04
6:23 p.m.
On 18. Oct 2004, at 16:01, Michael Sheets wrote:
There already is 2 pixels?!?
Sorry, I meant 2-3 more, not total. If the small padding is so good why is there more on the top? ;)
That's a bug! ;)
Well, I think I initially did 6 pixels on each of the sides, but when I added gutter-stuff, I made it 2 pixels between folding-markers and end of gutter (and/or line numbers etc.), so I removed some to make it symmetrical.
I don't like too much padding, e.g. NSTextView seems to be using 1.5 times the width of a character or so, and that makes it hard for me to see how much stuff is indented.
But I can probably be persuaded to add two more pixels.
Kind regards Allan