support setting specific charset for decoding source file or stream

[coder-chenzhi]

Current charset used for decoding and encoding is hard-coded 'UTF-8'. This patch enables setting the charset used to decode source file from system properties. Other i/o operations, such as writing temporary file and reading output of external tools, still use hard-coded 'UTF-8' as the default charset.

Please review this patch.

BTW, the charset of source files can be changed in some revisions, actually. It will be better to support setting source file charset and destination file charset separately. However, it is not trivial to achieve. Because only the client knows which charset should be used for decoding in this situation, some core APIs, including Generators.getTree(String file) and Generators.getTree(String generator, String file), and the caller of them may be required modification.

[coveralls]

Coverage decreased (-0.01%) to 55.603% when pulling db4ec93 on coder-chenzhi:bugfix into 5b8490c on GumTreeDiff:develop.

[jrfaller]

Thanks for the PR, however we will implement that in an other way!