printer: ensure that we generate enough digits for floats
When the number of digits was not specified, we were sometimes outputting a number that was exactly halfway between the exact value and the next higher float. When reading that number in again, one would get a different value due to rounding issues. Therefore, we now always output enough digits, so that the number can be reconstructed unambigously. Fixes #500.