Format: strange behavior of basic compacting boxes #7715
Comments
|
Comment author: @Octachron The documentated behavior and the implemented behavior are indeed at odd. This phenomenon is maybe easier to see by setting the margin to 20, and extending your examples by defining two new functions let f = Format.printf "@[<%s 2>a@ @[<v 2>(b@,c@,d)@]@ e@]@.";; As expected, the output of 'g ""' and 'g "hov"' differ g "" prints: a (b and g "hov" prints However, as you constated and contrarily to the documented behavior, 'f ""' and 'f "hov"' gives the same output. The critical difference between "f" and "g" is that the content of the box fits in one line for the function "f". In other words, the implemented behavior is If a structural box does not fit fully on a simple line, a break hint also splits the line if the splitting ``moves to the left''. Either the documentation or implementation should be updated to be synchronized with each other. |
|
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. |
|
Reopening as it will be closed by #9618 |
Original bug ID: 7715
Reporter: gmelquiond
Status: confirmed (set by @Octachron on 2018-01-29T22:56:03Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.06.0
Category: standard library
Bug description
About basic compacting boxes, the documentation of Format says:
"a break hint also splits the line if the splitting ``moves to the left'' (i.e. the new line gets an indentation smaller than the one of the current line)."
and the Bonichon-Weis paper agrees with it:
"if splitting the line reduces the current indentation, a break hint splits the line, even if there is still enough room left on the current line."
So, when executing
Format.printf "@[<2>a@ @[<v 2>(b@,c@,d)@]@ e@]@.";;
I expect the following output
a.(b
....c
....d)
..e
Indeed, even if there is still some space on the line starting with d, since the current indentation is 4 while the indentation of e is 2, the box containing e should be put on a new line. But in practice, the output is the same as for a hov box:
a.(b
....c
....d).e
Even stranger, since the width of the broken output above is 8, reducing the margin to 9 should not change the output. Yet it actually fixes the bug.
More generally, as long as there are sufficiently many boxes, the output eventually becomes as documented. For example, with the default margin of 78, the following code starts behaving correctly once 71 iterations are reached.
Format.printf "@[<2>a@ @[<v 2>(";
for i = 1 to 71 do Format.printf "b@," done;
Format.printf "b)@]@ e@]@.";;
The text was updated successfully, but these errors were encountered: