Yes, I'm sure that you are right. I remember the campaign to get TextIO.inputLine to return a string option instead of just a string (with the empty string being the indicator for end-of-file) and it was a bit of a battle.