The previous one was confusing and prone to buffer overflows, and didn't
work correctly with 16-decimal-digit numbers. The new one simply uses
snprintf with a standard format string.
The major change is that we don't always print a decimal point now.
Fortunately, JSON doesn't distinguish between integers and reals.
