If I press C-d at the end of the input, the input is seemed to be flushed, but no EOF is sent to the program. If however I press C-d once more, EOF is sent.
Why is the EOF not sent the first time I press C-d? Where is this behavior documented?
To experiment youself play with cat, here is an example:
$ cat
abc<C-d>abc<C-d>
$
C-d is the End-of-transmission (EOT) character:
In Unix the end-of-file character (by default EOT) causes the terminal driver to make available all characters in its input buffer immediately; normally the driver would collect characters until it sees an end-of-line character. If the input buffer is empty (because no characters have been typed since the last end-of-line or end-of-file), a program reading from the terminal reads a count of zero bytes. In Unix, such a condition is understood as having reached the end of the file.
In your example, when you run cat and type a few characters followed by C-d, the characters typed to that point are sent to cat which prints them to the screen. Now the input buffer is empty, so when you type C-d again, cat reads zero bytes from the buffer and terminates because the end-of-file condition has been met.
With bash you're probably using the readline library.
As you asked for the documentation, here it is
You'll see that Ctrl-D deletes the character underneath the cursor, and if you keep on reading, you'll discover lots of wonderful shortcuts!
