Wrong decimal separator (',') in JSON output in double/real type values at non-EN locales

[GoogleCodeExporter]

What steps will reproduce the problem?
1. setlocale(LC_ALL, 'pl_PL') - at main php script level (eg. index.php ) 
2. $v = '12.345'; $v = (double)$v;
3. echo $v; // prints 12,345

Probably this is true for any language/locale using comma instead dot as 
decimal separator.

I've tested on PHP 5.2.3, Linux 2.6.21.5-smp on Sun E450 hardware

Small patch resolve this problem:
vistable.php from line 1919:
>$out = json_encode($this->response);
>$out = preg_replace('/"(new Date\(.*?\))"/', "$1", $out);
>$out = preg_replace('/([\{,])"([A-Za-z_][A-Za-z0-9_]*)"/', "$1$2", $out);
Add new one:
++ $out = preg_replace('/(v:\d+),(\d+)/', "$1.$2", $out);

Original issue reported on code.google.com by klawon.m...@gmail.com on 15 Nov 2010 at 10:20