From a42e4108ee9971200c292321ff4c7c0d13f10333 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 8 Jul 2015 11:51:35 +0000
Subject: [PATCH] More locale setting for outputting decimals in English.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10233 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/Values.java                              | 3 ++-
 prism/src/userinterface/properties/GraphConstantLine.java | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/prism/src/parser/Values.java b/prism/src/parser/Values.java
index 8d38adeb..89c25922 100644
--- a/prism/src/parser/Values.java
+++ b/prism/src/parser/Values.java
@@ -29,6 +29,7 @@ package parser;
 import java.text.DecimalFormat;
 import java.text.NumberFormat;
 import java.util.ArrayList;
+import java.util.Locale;
 
 import parser.ast.ModulesFile;
 import parser.type.Type;
@@ -485,7 +486,7 @@ public class Values //implements Comparable
 		String s;
 		
 		if (o instanceof Double) {
-			NumberFormat nf = new DecimalFormat();
+			NumberFormat nf = DecimalFormat.getInstance(Locale.UK);
 			nf.setMaximumFractionDigits(6);
 			s = nf.format(((Double)o).doubleValue());
 		} else {
diff --git a/prism/src/userinterface/properties/GraphConstantLine.java b/prism/src/userinterface/properties/GraphConstantLine.java
index 5dac5673..be45aa2d 100644
--- a/prism/src/userinterface/properties/GraphConstantLine.java
+++ b/prism/src/userinterface/properties/GraphConstantLine.java
@@ -33,6 +33,7 @@ import java.awt.Graphics;
 import java.awt.Insets;
 import java.text.DecimalFormat;
 import java.text.NumberFormat;
+import java.util.Locale;
 
 import javax.swing.DefaultListCellRenderer;
 import javax.swing.Icon;
@@ -88,7 +89,7 @@ public class GraphConstantLine extends javax.swing.JPanel
                         setIcon(null);
                         String str;
                         Double d = (Double) obj;
-                        NumberFormat n = new DecimalFormat();
+                        NumberFormat n = DecimalFormat.getInstance(Locale.UK);
                         n.setMaximumFractionDigits(6);
                         str = n.format(d.doubleValue());
                         setText((obj == null) ? "" : str);