Better escaping of null characters.

If a null character isn't followed by a digit, then it should be safe to
escape it using the shorter sequence "\0" instead of "\x00".

See #220.