Re: size of the slider bar

[Richard M. Stallman]

    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,  

This might work fast enough to be usable--I guess we could try it if
someone writes it.  It might be painfully slow when you visit a file.

    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 might cause other visible inconsistencies.
For instance, the position of the top of the slider would not
correspond correctly to the fraction of the buffer above the
top of the window.