From 4e9164de732917b0cdf820be36b43f3348cd7991 Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Thu, 16 Jan 2025 18:26:12 +0100 Subject: [PATCH] [kernel] Remove obsolete pp_print_string_fill --- src/libraries/utils/pretty_utils.ml | 9 --------- src/libraries/utils/pretty_utils.mli | 3 --- 2 files changed, 12 deletions(-) diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml index bac42ea030..df97d37c80 100644 --- a/src/libraries/utils/pretty_utils.ml +++ b/src/libraries/utils/pretty_utils.ml @@ -37,15 +37,6 @@ let to_string ?margin pp x = Format.pp_print_flush f () ; Buffer.contents b -let rec pp_print_string_fill out s = - if String.contains s ' ' then begin - let i = String.index s ' ' in - let l = String.length s in - let s1 = String.sub s 0 i in - let s2 = String.sub s (i+1) (l - i - 1) in - Format.fprintf out "%s@ %a" s1 pp_print_string_fill s2 - end else Format.pp_print_string out s - type sformat = (unit,Format.formatter,unit) format type 'a formatter = Format.formatter -> 'a -> unit type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli index 9082720f01..c169cbe4fd 100644 --- a/src/libraries/utils/pretty_utils.mli +++ b/src/libraries/utils/pretty_utils.mli @@ -57,9 +57,6 @@ val to_string: ?margin:int -> (Format.formatter -> 'a -> unit) -> 'a -> string (** {2 separators} *) -val pp_print_string_fill : Format.formatter -> string -> unit -(** transforms every space in a string in breakable spaces.*) - val escape_underscores : string -> string (* ********************************************************************** *) -- GitLab