void set_eof();
public:
- /** Returns the end-of-file flag. */
+ /** Returns the end-of-file flag. Note that some types of objects won't
+ indicate end-of-file until you try to read at least one byte past the actual
+ end, while others indicate it when you've read the last byte. */
bool eof() const { return eof_flag; }
/** Returns the system-level handle for the object. Used by Console to