How can I format and print a REAL_32 to the console? Similar to C sprintf. I'd like to set the number of decimals shown, so that e.g. 1.0000000000001 is shown instead of 1. Thx