[m-dev.] Idea: truncate trailing 0s when printing floats

[Ralph Becket]

Whenever I debug programs that manipulate floats, the output is usually
obscured with unnecessary trailing zeroes (fourteen of them if the float
has no fractional part).

I'd like to change the way we format floats in the following way:
- if a format specifier is supplied, do what we currently do
- otherwise do not print unnecessary trailing 0s.

So we would have
	string.format("%7.3f", [f(42.0)]) = " 42.000"
	string.format("%f", [f(42.0)])    = "42.0"
	string.format("%f", [f(42.1)])    = "42.1"

whereas currently we have
	string.format("%7.3f", [f(42.0)]) = " 42.000"
	string.format("%f", [f(42.0)])    = "42.00000000000000"
	string.format("%f", [f(42.1)])    = "42.10000000000000"

Can anyone see a problem with me making this change?

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------