Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Format: More refined check to evaluate whether a box shall lead to go beyond max_indent and need a break prior to opening? #7807
Original bug ID: 7807
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 coq/coq#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
Steps to reproduce