Merge pull request #9237 from gasche/format-update-geometry

Format.pp_update_geometry: formatter -> (geometry -> geometry) -> unit
master
Gabriel Scherer 2020-01-15 22:37:37 +01:00 committed by GitHub
commit 82d7971b4f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 49 additions and 12 deletions

View File

@ -57,6 +57,10 @@ Working version
- #8894: Added List.fold_left_map function combining map and fold.
(Bernhard Schommer, review by Alain Frisch and github user @cfcs)
- #9237: `Format.pp_update_geometry ppf (fun geo -> {geo with ...})`
for formatter geometry changes that are robust to new geometry fields.
(Gabriel Scherer, review by Josh Berdine and ???)
### Other libraries:
- #9106: Register printer for Unix_error in win32unix, as in unix.

View File

@ -815,29 +815,48 @@ let pp_set_margin state n =
(** Geometry functions and types *)
type geometry = { max_indent:int; margin: int}
let validate_geometry {margin; max_indent} =
if max_indent < 2 then
Error "max_indent < 2"
else if margin <= max_indent then
Error "margin <= max_indent"
else Ok ()
let check_geometry geometry =
geometry.max_indent > 1
&& geometry.margin > geometry.max_indent
match validate_geometry geometry with
| Ok () -> true
| Error _ -> false
let pp_get_margin state () = state.pp_margin
let pp_set_full_geometry state {margin; max_indent} =
pp_set_margin state margin;
pp_set_max_indent state max_indent;
()
let pp_set_geometry state ~max_indent ~margin =
if max_indent < 2 then
raise (Invalid_argument "Format.pp_set_geometry: max_indent < 2")
else if margin <= max_indent then
raise (Invalid_argument "Format.pp_set_geometry: margin <= max_indent")
else
pp_set_margin state margin; pp_set_max_indent state max_indent
let geometry = { max_indent; margin } in
match validate_geometry geometry with
| Error msg ->
raise (Invalid_argument ("Format.pp_set_geometry: " ^ msg))
| Ok () ->
pp_set_full_geometry state geometry
let pp_safe_set_geometry state ~max_indent ~margin =
if check_geometry {max_indent;margin} then
pp_set_geometry state ~max_indent ~margin
else
()
let geometry = { max_indent; margin } in
match validate_geometry geometry with
| Error _msg ->
()
| Ok () ->
pp_set_full_geometry state geometry
let pp_get_geometry state () =
{ margin = pp_get_margin state (); max_indent = pp_get_max_indent state () }
let pp_update_geometry state update =
let geometry = pp_get_geometry state () in
pp_set_full_geometry state (update geometry)
(* Setting a formatter basic output functions. *)
let pp_set_formatter_out_functions state {
out_string = f;
@ -1123,6 +1142,7 @@ and get_max_indent = pp_get_max_indent std_formatter
and set_geometry = pp_set_geometry std_formatter
and safe_set_geometry = pp_safe_set_geometry std_formatter
and get_geometry = pp_get_geometry std_formatter
and update_geometry = pp_update_geometry std_formatter
and set_max_boxes = pp_set_max_boxes std_formatter
and get_max_boxes = pp_get_max_boxes std_formatter

View File

@ -488,6 +488,19 @@ val safe_set_geometry : max_indent:int -> margin:int -> unit
@since 4.08.0
*)
(**
[pp_update_geometry ppf (fun geo -> { geo with ... })] lets you
update a formatter's geometry in a way that is robust to extension
of the [geometry] record with new fields.
Raises an invalid argument exception if the returned geometry
does not satisfy {!check_geometry}.
@since 4.11.0
*)
val pp_update_geometry : formatter -> (geometry -> geometry) -> unit
val update_geometry : (geometry -> geometry) -> unit
val pp_get_geometry: formatter -> unit -> geometry
val get_geometry: unit -> geometry
(** Return the current geometry of the formatter