Parse reals as string in JSON front-end

diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc
index d34a279442bd56250e268951c3de719970fc1d3d..629578c61d789ffb07bc5e57118f27348da56a3b 100644 (file)
--- a/frontends/json/jsonparse.cc
+++ b/frontends/json/jsonparse.cc
@@ -76,6 +76,7 @@ struct JsonNode
                        {
                                type = 'N';
                                data_number = ch - '0';
+                               data_string += ch;
 
                                while (1)
                                {
@@ -84,12 +85,39 @@ struct JsonNode
                                        if (ch == EOF)
                                                break;
 
+                                       if (ch == '.')
+                                               goto parse_real;
+
                                        if (ch < '0' || '9' < ch) {
                                                f.unget();
                                                break;
                                        }
 
                                        data_number = data_number*10 + (ch - '0');
+                                       data_string += ch;
+                               }
+
+                               data_string = "";
+                               break;
+
+                       parse_real:
+                               type = 'S';
+                               data_number = 0;
+                               data_string += ch;
+
+                               while (1)
+                               {
+                                       ch = f.get();
+
+                                       if (ch == EOF)
+                                               break;
+
+                                       if (ch < '0' || '9' < ch) {
+                                               f.unget();
+                                               break;
+                                       }
+
+                                       data_string += ch;
                                }
 
                                break;