Skip to content
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

Closed
vicuna opened this issue Feb 3, 2015 · 5 comments
Closed

Formatting tags are lost on a flush #6769

vicuna opened this issue Feb 3, 2015 · 5 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Feb 3, 2015

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;;

  • : unit = ()

printf "@{@{hello@}@}";;

hello- : unit = () # printf "@{@{hello@.@}@}";; hello - : unit = () #

Additional information

is also reproducible on 4.01

@vicuna
Copy link
Author

vicuna commented Mar 15, 2017

Comment author: @damiendoligez

The question is whether flush should close the currently open tags as well as the boxes.

@vicuna
Copy link
Author

vicuna commented Mar 15, 2017

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 flush functions - hard_flush and flush. The hard_flush may break the first invariant (syntax and semantics), but will never violate the second one. It should be used at the end of the program, or other already exceptional/abnormal conditions. The normal flush function, will always preserve the first invariant, although the second one will be relaxed. Basically, a flush ppf is a recommendation to flush data as soon as possible.

@vicuna
Copy link
Author

vicuna commented Jun 6, 2018

Comment author: @pierreweis

This has been solved on 2016/05/24.

@vicuna
Copy link
Author

vicuna commented Jun 6, 2018

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.

@vicuna
Copy link
Author

vicuna commented Jun 6, 2018

Comment author: @pierreweis

Resolved for two years and no complaint reported => close it!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants