From 91d9c50bb30583cbaad09620a42c0d8fe2421273 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 26 Sep 2017 14:37:03 +0200
Subject: [PATCH] Parse reals as string in JSON front-end

---
 frontends/json/jsonparse.cc | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc
index d34a27944..629578c61 100644
--- a/frontends/json/jsonparse.cc
+++ b/frontends/json/jsonparse.cc
@@ -76,6 +76,34 @@ struct JsonNode
 			{
 				type = 'N';
 				data_number = ch - '0';
+				data_string += ch;
+
+				while (1)
+				{
+					ch = f.get();
+
+					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)
 				{
@@ -89,7 +117,7 @@ struct JsonNode
 						break;
 					}
 
-					data_number = data_number*10 + (ch - '0');
+					data_string += ch;
 				}
 
 				break;