diff options
| -rw-r--r-- | stdlib/format.ml | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/stdlib/format.ml b/stdlib/format.ml index eadf20069..7a46c31ca 100644 --- a/stdlib/format.ml +++ b/stdlib/format.ml @@ -187,20 +187,23 @@ let pp_clear_queue state = (* Pp_infinity: large value for default tokens size. Pp_infinity is documented as being greater than 1e10; to avoid - confusion about the word ``greater'' we shoose pp_infinity greater - than 1e10 + 1; for correct handling of tests in the algorithm - pp_infinity must be even one more than that; let's stand on the + confusion about the word ``greater'', we choose pp_infinity greater + than 1e10 + 1; for correct handling of tests in the algorithm, + pp_infinity must be even one more than 1e10 + 1; let's stand on the safe side by choosing 1.e10+10. Pp_infinity could probably be 1073741823 that is 2^30 - 1, that is - the minimal upper bound of integers; now that max_int is defined, - could also be defined as max_int - 1. - - We must carefully double-check all the integer arithmetic - operations that involve pp_infinity before setting pp_infinity to - something around max_int: otherwise any overflow would wreck havoc - the pretty-printing algorithm's invariants. - Is it worth the burden ? *) + the minimal upper bound for integers; now that max_int is defined, + this limit could also be defined as max_int - 1. + + However, before setting pp_infinity to something around max_int, we + must carefully double-check all the integer arithmetic operations + that involve pp_infinity, since any overflow would wreck havoc the + pretty-printing algorithm's invariants. Given that this arithmetic + correctness check is difficult and error prone and given that 1e10 + + 1 is in practice large enough, there is no need to attempt to set + pp_infinity to the theoretically maximum limit. Is it not worth the + burden ! *) let pp_infinity = 1000000010;; |