Browse Source

parser.Values: use PrismUtils.formatDouble for double formatting

Fixes issue #1.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11760 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
3b4cb29c2c
  1. 5
      prism/src/parser/Values.java

5
prism/src/parser/Values.java

@ -37,6 +37,7 @@ import parser.type.TypeDouble;
import parser.type.TypeInt; import parser.type.TypeInt;
import prism.ModelInfo; import prism.ModelInfo;
import prism.PrismLangException; import prism.PrismLangException;
import prism.PrismUtils;
/** /**
* Class to store a list of typed constant/variable values. * Class to store a list of typed constant/variable values.
@ -486,9 +487,7 @@ public class Values //implements Comparable
String s; String s;
if (o instanceof Double) { if (o instanceof Double) {
NumberFormat nf = DecimalFormat.getInstance(Locale.UK);
nf.setMaximumFractionDigits(6);
s = nf.format(((Double)o).doubleValue());
s = PrismUtils.formatDouble((double)o);
} else { } else {
s = o.toString(); s = o.toString();
} }

Loading…
Cancel
Save