CBFalconer wrote:
Waldek Hebisch wrote:
... snip ...
So, IMHO the following program is correct (and works with the patch):
program fjf490b(Output);
var t: Text; c: Char;
begin Rewrite (t); Reset (t);
I disagree. At this point t is open, and using lazy i/o a get is pending.
You mix the standard with implementation details. Standard suggests, but does not requre lazy i/o. Basic criterion for correctness of lazy i/o is that programs working without lazy i/o should still work. So, from this point `t^' should be available to the programmer (read the postcondition of `Reset'). The standard says that content of `t^' is undefined (since t is at eof), which in plain language means that the implementation should put some garbage into it. AFAICS if you do not want to look at the garbage, you need explicitly test for eof.
c := t^;
To implement this the system should perform the actual get. The get fails, because the file is at EOF, signalling "attempt to read past EOF". It has nothing to do with the definedness of t^. Similarly eoln(t) should fail.
Note that accessing `t^' is logically quite different from `get'. Remember that `t^' references a record _after_ current file position. At this point `get' would attempt to move file position past the end of file and access _second_ record past the end of file, which indeed is an error. `eoln' is different.
Accessing f^, or executing eoln or any read on t, should call something that checks whether a get is pending, and executes it if so. This is a library issue. The compiler issure is to make sure that the f^ action calls the routine, which should return the pointer. You cannot have lazy i/o and just access the file pointer as another address.
All the magic has to be in the compiler and the runtime. The user can treat the file buffer almost like another variable.