Source files can be in any coding system, provided Python can
read a coding: line at the beginning of the file. So source files
should be loaded in binary format and decoded according to that
line, not assumed to be in the default coding system.
Fixes#398.