Fix JSON NaN

Hi,

The attached patch fixes the JSON generation when dealing with NaN (not
a number), this makes the JSON parsing in the web browser succeed
(before it would get a "nan" which is not a valid JS value)

Chris