From 9ea91f2dd2c59b8355cdb03440e57c82aebabc76 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 25 Oct 2016 15:13:40 +0000 Subject: [PATCH] PrismUtils.formatDouble: Improve previous commit, strip trailing zeros for .xxx0000 as well We want to strip trailing zeros (after the .) as well. This commit, together with the previous one should provide the previous functionality, but fixing the issue with trailing zeros for integers. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11860 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismUtils.java | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index 912e6c9c..e658ec07 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -200,8 +200,17 @@ public class PrismUtils public static String formatDouble(double d) { // 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"); + // To match C's printf, we have to tweak the Java version, + // strip trailing zeros after the . + String result = String.format(Locale.UK, "%.12g", d); + // if there are only zeros after the . (e.g., .000000), strip them including the . + result = result.replaceFirst("\\.0+(e|$)", "$1"); + // handle .xxxx0000 + // we first match .xxx until there are only zeros before the end (or e) + // as we match reluctantly (using the *?), all trailing zeros are captured + // by the 0+ part + result = result.replaceFirst("(\\.[0-9]*?)0+(e|$)", "$1$2"); + return result; } /** @@ -210,10 +219,19 @@ public class PrismUtils public static String formatDouble(int prec, double d) { // 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"); + // To match C's printf, we have to tweak the Java version, + // strip trailing zeros after the . + String result = String.format(Locale.UK, "%." + prec + "g", d); + // if there are only zeros after the . (e.g., .000000), strip them including the . + result = result.replaceFirst("\\.0+(e|$)", "$1"); + // handle .xxxx0000 + // we first match .xxx until there are only zeros before the end (or e) + // as we match reluctantly (using the *?), all trailing zeros are captured + // by the 0+ part + result = result.replaceFirst("(\\.[0-9]*?)0+(e|$)", "$1$2"); + return result; } - + /** * Create a string for a list of objects, with a specified separator, * e.g. ["a","b","c"], "," -> "a,b,c"