Format.pp_update_geometry: formatter -> (geometry -> geometry) -> unit #9237
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
(cc @Octachron and any other benevolent reviewer) There are two small refactoring commits in this PR, so it is best reviewed commit-by-commit. |
jberdine
reviewed
Jan 10, 2020
gasche
force-pushed
the
format-update-geometry
branch
2 times, most recently
from
43eef20
to
5cf7790
Compare
jberdine
reviewed
Jan 10, 2020
Octachron
approved these changes
Jan 14, 2020
|
|
||
| let pp_get_margin state () = state.pp_margin | ||
|
|
||
| let pp_set_full_geometry state {margin; max_indent} = |
There was a problem hiding this comment.
I am not sure if full is the right adjective here: maybe unsafe? Or an adverb directly?
There was a problem hiding this comment.
I'll leave it as-is: this is not exposed in the public API, and the _full prefix will become self-evident after we start adding extra record fields, while pp_set_geometry is left partial due to backward-compatibility constraints.
gasche
force-pushed
the
format-update-geometry
branch
from
3894550
to
bc574f5
Compare
This lets users write code that is robust to the addition of new
geometry fields.
Format.(pp_update_geometry ppf (fun geo -> {geo with ...}))
Today the only way to set the geometry is
Format.pp_set_geometry ppf ~margin ~max_indent
we cannot add optional parameters after the [ppf] argument, and adding
new labeled parameters would break user code.
(Also: it's often convenient to work with the record directly, for
example to reset a previous geometry saved with [pp_get_geometry];
this is indirectly provided by [pp_update_geometry].)
|
(The CI failure on AppVeyor appears to be due to memprof, and thus unrelated.) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This lets users write code that is robust to the addition of new
geometry fields.
Today the only way to set the geometry is
we cannot add optional parameters after the [ppf] argument, and adding
new labeled parameters would break user code.
(Also: it's often convenient to work with the record directly, for
example to reset a previous geometry saved with [pp_get_geometry];
this is indirectly provided by [pp_update_geometry].)