Digest #168 2021-11-02
Contributions
The "0 <= u2 <= u1" is misleading. As becomes clear from the rest, 0 <= u2 < u1 is also guaranteed if the line terminator starts before u1 chars are received.
READ-LINE reads at most u1 characters that are not part of the line terminator. Line terminators of up to 2 chars can occur (i.e., CRLF). However, even with such a line terminator, it's enough to read u1+1 chars: if the line terminator does not start at the last char in the buffer, READ-LINE does not need to know if a line terminator follows right afterwards: It just returns u2=u1, no need to know about line terminators.
At least in Linux it is significantly faster to use input buffering than to always read u1+1 characters using a system call and reposition the file with another system call.
Acknowledgments: Discussions with ruv and dxforth resulted in this comment.