New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Format: More refined check to evaluate whether a box shall lead to go beyond max_indent and need a break prior to opening? #7807
Comments
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
I encountered this problem trying to figure out why the forthcoming support in Orsetto for the CBOR diagnostic notation was producing poorly indented object and array elements when I was using any kind of "horizontal or vertical" box mode instead of |
Very few people are interested in working on the Format codebase today. Your problem sounds real (just as the initial report), but it is not likely to get fixed if you don't submit a patch/pull request yourself. In the meantime I will reopen the bug report to get this issue more visibility -- but if it gets closed again for inactivity, I won't fight for it. |
Before I investigate, how exhaustive is the test suite for the |
Basic functionality is tested in
There are also existing alternatives to Format that you may want to evaluate for your needs first, notably PPrint. Note however that one reason why people keep using Format is that its |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7807
Reporter: herbelin
Status: new
Resolution: open
Priority: normal
Severity: feature
Version: 4.06.1
Category: standard library
Related to: #7862
Monitored by: ralfj @gasche @yakobowski
Bug 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 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
Format.format_pp_token
, is the "size" computed in thePp_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.Steps to reproduce
See #7804 for a simplified example, or coq/coq#7731 for a realistic example.
The text was updated successfully, but these errors were encountered: