Editorial fixes.

This includes removing trailing blanks; sorry about this, but I'd say all
other edits are about as trivial, and so perhaps it's ok to have a mixed
whitespace/non-whitespace commit.  For reviewing, consider git diff -w.