Encode floating point numbers as short as possible

Floating point numbers are no longer encoded as a one to one mapping
of their binary representation, but as short as possible (while still
being acurate). The double-conversion library [1] is used to do the
hard work.

The ECMAScript compatible conversion is used.

[1] https://code.google.com/p/double-conversion/

I'm not much of a C/C++ coder yet, so please have a close look if I'm doing something stupid.