Re: Fwd: size of the slider bar

[Stefan Monnier]

> I'm sure you know that the ratio of the length of this bar to the total
> length of the scroll bar must represent the ratio between the number of
> lines in the window to the number of lines in the file.  So, the ratio,
> and therefore the length of this bar, must remain the same so long as
> neither the number of lines in the file nor the height of the window
> are changed.

We know you think this way, but it seems you somehow still haven't realized
that you're wrong:
1 - there's nothing that says it *should be* related to the ratio of the
    number of lines, rather than chars.
2 - the number of lines displayed is not constant either, so even if we
    switched to lines (which could be costly) it wouldn't be enough: we need
    the ratio of the number of *pixels*.

In either case, this would be way too expensive to compute, especially when
compared to the benefit.


        Stefan