diff --git a/Makefile.generating b/Makefile.generating index 8d64ab4a1b478b122fa801de067c40717b3d9f6d..e1793bede2262382953381b03a1e62734623a165 100644 --- a/Makefile.generating +++ b/Makefile.generating @@ -133,6 +133,7 @@ ifeq ($(HAS_OCAML408),yes) Format.String_tag str -> str \ | _ -> raise (Invalid_argument "unsupported tag extension") FORMAT_STAG_OF_STRING=Format.String_tag s + FORMAT_PP_OPT=Format.pp_print_option HAS_OCAML407_OR_408=yes else DYNLINK_INIT=Dynlink.init @@ -144,6 +145,10 @@ else else HAS_OCAML407_OR_408=no endif + FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \ + match o with \ + | None -> none fmt () \ + | Some v -> pp fmt v endif ifeq ($(HAS_OCAML407_OR_408),yes) @@ -169,6 +174,7 @@ src/libraries/stdlib/transitioning.ml: \ -e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \ -e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \ -e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \ + -e 's/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g' \ $< > $@ $(CHMOD_RO) $@ diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml index 3903899e1fe7b0849642f16e48a5fbfdbbb60c14..f7ea40bd18f2c9b3c9e3acf4a2369ae078021e2e 100644 --- a/src/kernel_services/ast_printing/cabs_debug.ml +++ b/src/kernel_services/ast_printing/cabs_debug.ml @@ -250,17 +250,17 @@ and pp_raw_stmt fmt = function pp_block bl1 pp_block bl2 pp_cabsloc loc | THROW(e,loc) -> fprintf fmt "@[<hov 2>THROW %a, loc(%a)@]" - (Pretty_utils.pp_opt pp_exp) e pp_cabsloc loc + (Transitioning.Format.pp_print_option pp_exp) e pp_cabsloc loc | TRY_CATCH(s,l,loc) -> let print_one_catch fmt (v,s) = fprintf fmt "@[<v 2>@[CATCH %a {@]@;%a@]@;}" - (Pretty_utils.pp_opt pp_single_name) v + (Transitioning.Format.pp_print_option pp_single_name) v pp_stmt s in fprintf fmt "@[<v 2>@[TRY %a (loc %a) {@]@;%a@]@;}" pp_stmt s pp_cabsloc loc - (Pretty_utils.pp_list ~sep:"@;" print_one_catch) l + (Format.pp_print_list ~pp_sep:Format.pp_print_cut print_one_catch) l | CODE_ANNOT (_,_) -> fprintf fmt "CODE_ANNOT" | CODE_SPEC _ -> fprintf fmt "CODE_SPEC" diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in index 779da76ce9aedbc0c12ad68d06cf6dc93938e632..6d95b7a1466454402704bd22f262d9bb770d5096 100644 --- a/src/libraries/stdlib/transitioning.ml.in +++ b/src/libraries/stdlib/transitioning.ml.in @@ -78,6 +78,8 @@ module Format = struct Format.pp_open_@FORMAT_STAG@ fmt s let pp_close_stag fmt () = Format.pp_close_@FORMAT_STAG@ fmt () + + let pp_print_option = @FORMAT_PP_OPT@ end module Q = struct diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli index 03507b2d2cc3ab5497c323f851e3fa94dc3939c7..bc07a75fdb6ff3168bb568339241dc4b0403b8af 100644 --- a/src/libraries/stdlib/transitioning.mli +++ b/src/libraries/stdlib/transitioning.mli @@ -74,6 +74,8 @@ module Format: sig Format.formatter -> unit -> formatter_stag_functions val pp_open_stag : Format.formatter -> stag -> unit val pp_close_stag : Format.formatter -> unit -> unit + val pp_print_option: ?none:(Format.formatter -> unit -> unit) -> + (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a option -> unit end (** {1 Zarith} *)