Browse Source

Fix in PrismUtils.formatDouble methods: Only remove trailing .000 not trailing zeros for integers [with Linda Leuschner]

The regular expression for identifying the trailing .0* part of the string
did not require the . to actually occur, which would also strip the zeros from
integers ending with zeros.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11859 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
d960f4b513
  1. 4
      prism/src/prism/PrismUtils.java

4
prism/src/prism/PrismUtils.java

@ -201,7 +201,7 @@ public class PrismUtils
{
// Use UK locale to avoid . being changed to , in some countries.
// To match C's printf, we have to tweak the Java version (strip trailing .000)
return String.format(Locale.UK, "%.12g", d).replaceFirst("\\.?0+(e|$)", "$1");
return String.format(Locale.UK, "%.12g", d).replaceFirst("\\.0+(e|$)", "$1");
}
/**
@ -211,7 +211,7 @@ public class PrismUtils
{
// Use UK locale to avoid . being changed to , in some countries.
// To match C's printf, we have to tweak the Java version (strip trailing .000)
return String.format(Locale.UK, "%." + prec + "g", d).replaceFirst("\\.?0+(e|$)", "$1");
return String.format(Locale.UK, "%." + prec + "g", d).replaceFirst("\\.0+(e|$)", "$1");
}
/**

Loading…
Cancel
Save