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
Formatting tags are lost on a flush #6769
Comments
Comment author: @damiendoligez The question is whether |
Comment author: @ivg Tags represent semantics (i.e., what is data about), where boxes represent the syntax (i.e., how it is printed; how it looks like). Intuitively, the flush operation should be transparent with respect to the syntax and semantics of data. So the same program with and without interleaved flushes should have the same final output. This is the first invariant. Another intuitive property is that flush should dump all available data. This is the second invariant. It is not trivial to preserve both these properties with respect to boxes since we can't layout a stream that has non-closed boxes. A possible solution is to provide two |
Comment author: @pierreweis This has been solved on 2016/05/24. |
Comment author: @pierreweis When flushing, the pretty-printer engine now automatically closes all open semantic tags. This is consistent to the treatment of pretty-printing boxes that are all closed before rendering available material. Note that closing a semantic tag may output arbitrary text (close tag printing and marking). Hence, the rendering engine now automaticall adds new material to the output. One can argue that automatically closing semantic tags and adding material to the output may surprise the user and hurt the program normal behavior; however, not closing a semantic tag is most likely a bug and the new behavior will reveal the problem and help to fix it. |
Comment author: @pierreweis Resolved for two years and no complaint reported => close it! |
Original bug ID: 6769
Reporter: @ivg
Assigned to: @pierreweis
Status: closed (set by @pierreweis on 2018-06-06T08:58:06Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.1
Category: standard library
Monitored by: @hcarty
Bug description
I'm not sure whether it is a bug or feature, but if you flush formatter, it will "forget" all its tags.
Steps to reproduce
set_tags true;;
printf "@{@{hello@}@}";;
hello- : unit = () # printf "@{@{hello@.@}@}";; hello - : unit = () #Additional information
is also reproducible on 4.01
The text was updated successfully, but these errors were encountered: