Re: size of the slider bar

[Stefan Monnier]

> 1) Keep an index with line numbers for every 5000th character in a  buffer
>    and use the index to get a good approximate translation from
>    char-position to line number (or char-position to pixel height count,
>    i.e. lines x char-height) by using the index and counting the  remaining
>    few lines. The index could be updated through one mean or  the other, but
>    it's enough to keep it approximately right.

[ As mentioned, counting lines is not enough, we need to count pixels. ]
Note that the "lines" we need to count are not just separated by \n
(i.e. internal lines as counted by `count-lines') but are screen lines,
which depend on text-properties, on the frame's default font, on the
window's width, ...  so counting the "total number of lines" is very costly
since it requires rendering the whole buffer.

> 2) Do not change the slider size WHILE it is being dragged, because that
> is confusing from an UI point of view. I think it would be less confusing
> to adapt it AFTER dragging.

This is indeed the way to go.  But note that adapting the size of the thumb
after it's dragged will also adapt its position (the extreme case: your
slider originally takes 10% of the whole height and you scroll to the bottom
of the buffer and the last "char" is a large image: right before releasing
the drag, the thumb will be at position 90% and size 10%, and after
releasing the drag it'll be at position 99% and size 1%).


        Stefan