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
Possible bug in Format #7862
The second call to "print_space" in "Steps To Reproduce" generates a trailing space even though the line is broken. Moreover, removing either
results in "correct" behavior (the line is not broken).
Steps to reproduce
Output (there is a trailing space in the second line):
Comment author: @alainfrisch
Note that the doc says:
[pp_print_space ppf ()] emits a 'space' break hint: the pretty-printer may split the line at this point, otherwise it prints one space.
which indeed suggests that the expected behavior is that the space should not be printed when the pretty-printer does split the line (and this is what usually happens).
Comment author: bvaugon
It seems that there is two problems: an "unwanted trailing space" and a "suprising line break".
Concerning the "surprising line break" that is automatically inserted by the open_box once the current line size exceed 68 characters (68 = default_margin - default_min_space_left), it is configurable through the "min_space_left" property:
(* Minimal space left before margin, when opening a box. *)
using the Format.set_max_indent function :
where max_indent = margin - space_left.
Remarks that calling pp_set_max_indent with an argument greater or equal than margin has no effect.
Comment author: @nojb
I am not sure about that, because if I remove the code that prints the first line, then there is no break between second and third line, which tells me that there is enough space and a break is not warranted there.
In other words: maybe the trailing space is correct and the problem is the break that shouldn't happen.
Comment author: bvaugon
In fact, when you remove the code that prints the first line, there is no break but it should be (or the documentation should be fixed). Indeed, opening a box after the 68th character should not be allowed following the comment "pp_min_space_left: minimal space left before margin when opening a box".
Furthermore (I don't know if there is a link with the other problems), opening a box at this positions seems to break vertical alignement like in the text printed by the following code:
q qzzzzzzzzzzzzzzzzzzzqzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzfffaaa A
A and B should be aligned.
Comment author: @Octachron
This is due to the current behavior of max_indent: it rejects to the left boxes opened beyond max_indent (if the enclosing box does not fit on the line). In particular, it does not try to understand if the opened box could fit on the line, see #7807 .
bvaugon, for your second example, this is due to the fact that max_indent limits the maximum indentation of the value.