|Anonymous | Login | Signup for a new account||2019-01-17 17:42 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007804||OCaml||standard library||public||2018-06-10 10:32||2018-06-11 21:41|
|Status||resolved||Resolution||no change required|
|Target Version||Fixed in Version|
|Summary||0007804: In the format library, are boxes intended to implicitly break?|
|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@]@.@.";
The output is
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.
|Tags||No tags attached.|
|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 http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html#1_Maximumindentationlimit [^] (amended by 0007720 and https://github.com/ocaml/ocaml/pull/1596 [^]), boxes opened at a position greater than 2 are rejected to the left if the englobing box does not fit on the left.|
|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.|
|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.|
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.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.
|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.|
Hi, we discussed further the issue at https://github.com/coq/coq/issues/7731 [^] [^] 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 format.ml). 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).
|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.|
|OK, I opened a feature request at 7807.|
|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|