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/