Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007804OCamlstandard librarypublic2018-06-10 10:322018-06-11 21:41
Assigned Tooctachron 
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.06.1 
Target VersionFixed in Version 
Summary0007804: In the format library, are boxes intended to implicitly break?
DescriptionI 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 ReproduceExecuting the following shows the issue:
for i = 4 to 7 do
Format.set_margin i; Format.printf "@[a@ #@[b@]@ c@]@.@.";

The output is

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 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.
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0007720assignedoctachron Format: spurious space at end of line 

-  Notes
octachron (developer)
2018-06-10 11:02

This is the expected behavior: `Format.set_margin 4` fixes the maximum box indentation to 2 and further calls to set_margin does not change the value of the maximum box indentation. Then as explained in [^] (amended by 0007720 and [^]), boxes opened at a position greater than 2 are rejected to the left if the englobing box does not fit on the left.
herbelin (reporter)
2018-06-10 12:19

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 `set_margin`). Thanks again.
octachron (developer)
2018-06-10 12:35

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.
herbelin (reporter)
2018-06-10 13:33

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;
Format.set_max_indent 10;
Format.printf " @[aaaaaaaaaaa@ #@[b@]@ c@]@.@."

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.
octachron (developer)
2018-06-10 14:02

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.
herbelin (reporter)
2018-06-11 17:48

Hi, we discussed further the issue at [^] [^] and we catch a glimpse of how the formatting algorithm could maybe slightly be improved though.

The question is about the specification of `max_indent`. Is `max_indent` suppose to give the limit to indentation (as the name suggests) or to give a limit to box opening?

What seems to happen in the algorithm is that no box is opened beyond `max_ident` (line 352 of the current version of However, there might be boxes which do not lead to breaks, because the whole contents of the box fits without needing a break. Would such situation considered to be respectful of the `max_indent` specification?

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 `break` in this outer box and that this preceding `break` already checked that it was not necessary to break the line to display the forthcoming contents and thus, that the inner box which is part of this forthcoming contents shall not need to add a break itself and shall not violate the max_indent limit?

Hoping that my words are clear enough (it is not so easy to explain).
octachron (developer)
2018-06-11 20:59

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.
herbelin (reporter)
2018-06-11 21:41

OK, I opened a feature request at 7807.

- Issue History
Date Modified Username Field Change
2018-06-10 10:32 herbelin New Issue
2018-06-10 10:56 octachron Relationship added duplicate of 0007720
2018-06-10 11:02 octachron Note Added: 0019171
2018-06-10 12:19 herbelin Note Added: 0019172
2018-06-10 12:35 octachron Note Added: 0019173
2018-06-10 13:33 herbelin Note Added: 0019174
2018-06-10 14:02 octachron Note Added: 0019175
2018-06-11 14:29 octachron Status new => resolved
2018-06-11 14:29 octachron Resolution open => no change required
2018-06-11 14:29 octachron Assigned To => octachron
2018-06-11 17:48 herbelin Note Added: 0019181
2018-06-11 20:59 octachron Note Added: 0019182
2018-06-11 21:41 herbelin Note Added: 0019183

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker