Thanks for your input. I have a hard time regarding this as an "interactive" context, but I guess the moral of the story is that eof() only works if it's an honest-to-God file. The fact that it blocks seems to me completely contrary to the whole point of the function. The system IO is what I was hoping to avoid, but it looks like I can't.