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
In the format library, are boxes intended to implicitly break? #7804
Comments
Comment author: @Octachron This is the expected behavior: |
Comment author: herbelin Thanks for the quick answer. I still don't understand well if this is because it would be too complicated/costly to implement a preference given to the explicitly given break hints but I'm at least taking your answer as a confirmation that this is the official specification of the algorithm (of course the phenomenon is not tied to small values of |
Comment author: @Octachron It is not so much a question of complexity than a question of specification. Note also that the problem only appears with small values of max_indent, setting max_indent to margin - 1 (or margin - small_offset) generally avoids the issue. |
Comment author: herbelin It depends if by small you mean small in the absolute or relatively small. When I observed the phenomenon first, I had margin 78 and max_indent 49. For instance, the following also triggers the problem: Format.set_margin 15; but for 15 > max_indent > 10, I don't see the problem any more. Are you saying that with a sufficiently relatively large value of max_indent, I can ensure that the box would let the explicit break hints do their job? Thanks in advance for further help. |
Comment author: @Octachron I would say that you probably want to fix the max_indent value to margin - offset with a small value of offset (the starting value is 10). The maximum indentation value is here as a safety net to avoid opening a box at a position where there is not enough space left to print the box in a readable way. There is no way to disable this mechanism, but it would happen less frequently with small values of margin - max_indent. |
Comment author: herbelin Hi, we discussed further the issue at coq/coq#7731 [^] and we catch a glimpse of how the formatting algorithm could maybe slightly be improved though. The question is about the specification of What seems to happen in the algorithm is that no box is opened beyond If yes, it seems to me (within the limits of my understanding of the algorithm) that the question is whether it would be possible to make a finer test to decide if the opening of a box should insert an initial break or not. For instance, could it be possible to detect that we are in an outer box with a preceding Hoping that my words are clear enough (it is not so easy to explain). |
Comment author: @Octachron I agree that the algorithm could be improved. I would suggest to open a separate ticket as a feature request with a link to the problematic Coq examples and a good specification of the requested behavior. But I am not sure if Format's current maintainer is open to such modification. |
Comment author: herbelin OK, I opened a feature request at 7807. |
Original bug ID: 7804
Reporter: herbelin
Assigned to: @Octachron
Status: resolved (set by @Octachron on 2018-06-11T12:29:44Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.06.1
Category: standard library
Duplicate of: #7720
Related to: #7913
Monitored by: ralfj @gasche
Bug description
I have an example of a hov box containing a box where the split is not done at the break hints of the outer box but at the position of the opening of the inner box. This looks strange but maybe this is how it is supposed to work (I did not find documentation about it).
Steps to reproduce
Executing the following shows the issue:
<<
for i = 4 to 7 do
Format.set_margin i; Format.printf "@[a@ #@[b@]@ c@]@.@.";
done
The output is
<<
a
#b
c
a #
b c
a #
b c
a #b c
which shows that in the second and third case, a break is introduced by the inner box, while, intuitively, the break should have been done at the break hints of the outer box.
Apparently, this is due to the test "insertion_point > state.pp_max_indent" in function format_pp_token of format.ml. Couldn't have the lack of enough space detected already at the time of considering the preceding "official" break hint?
I shall use a workaround on my side but I'm still reporting it as I did not succeed to get an opinion on whether this is normal or not.
The text was updated successfully, but these errors were encountered: