|Description||This is a followup of a discussion at issue 7804 showing the example of a box which would fit on the line but which however forces a break just because it is opened beyond the max_indent limit.|
Assuming that the specification of max_indent is strictly to not indent beyond the max_indent value, the test made at box opening to force a break if the box is opened beyong max_indent seems overly preventive. Opening a box does not mean that printing the contents of the box shall necessarily need to break a line and indent.
In particular, in a situation such as described in https://github.com/coq/coq/issues/7731, [^] where a box is opened beyond the max_indent limit but this box is within a surrounding box and a previous break in the surrounding box has already checked that the forthcoming comments shall fit, the box may (??) trust the decision take by the previous break and not test max_indent. Would it make sense to refine the algorithm in this way? Otherwise said, looking at the implementation of `Format.format_pp_token`, is the "size" computed in the `Pp_break` clause correct enough to ensure that, if it fits, forthcoming boxes shall fit and shall not have to preventively test whether they are beyond the max_indent limit.