Changed JSONNumber to always uses JavaScript-level double->String conversion
  1) more JavaScripty
  2) works around inconsistency in String.valueOf(double) in hosted and web mode.

Review by: bruce


git-svn-id: https://google-web-toolkit.googlecode.com/svn/trunk@1965 8db76d5a-ed1c-0410-87a9-c151d255dfc7