diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml index 80fc744acfe0f71e1fb5cbf39b0c6f8f729251b0..798d70dbf8efefaf322161fef1955b3d7b76890a 100644 --- a/src/kernel_services/plugin_entry_points/plugin.ml +++ b/src/kernel_services/plugin_entry_points/plugin.ml @@ -381,7 +381,7 @@ struct let file ?error f = let dir = dir ?error () in - Datatype.Filepath.of_string ((dir :> string) ^ "/" ^ f) + Datatype.Filepath.concat dir ("/" ^ f) end diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml index 0e55cdc83a9a3c677e037f41c532c1b1cf8915c4..417d5f8ea3732f93a672361ffce2d830768e2137 100644 --- a/src/libraries/datatype/datatype.ml +++ b/src/libraries/datatype/datatype.ml @@ -1944,6 +1944,7 @@ module Filepath = struct let dummy = Filepath.Normalized.unknown let of_string ?existence ?base_name s = Filepath.Normalized.of_string ?existence ?base_name s + let concat ?existence t s = Filepath.Normalized.concat ?existence t s let pp_abs = Filepath.Normalized.pp_abs end diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli index 4243c2b50b18686b1cc07faf838b4a010923d605..9d659f95aaa1095a5d1e5ee0ab351e27e82393f5 100644 --- a/src/libraries/datatype/datatype.mli +++ b/src/libraries/datatype/datatype.mli @@ -349,6 +349,7 @@ val integer: Integer.t Type.t module Filepath: sig include S_with_collections with type t = Filepath.Normalized.t val of_string: ?existence:Filepath.existence -> ?base_name:string -> string -> t + val concat: ?existence:Filepath.existence -> t -> string -> t val pp_abs: Format.formatter -> t -> unit val dummy: t end diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml index 2a181a564731b5f39500545f75915577cab947ff..1fc3781fcc95176e4dbf3d46593dca96503cf777 100644 --- a/src/libraries/utils/filepath.ml +++ b/src/libraries/utils/filepath.ml @@ -235,7 +235,9 @@ let is_relative ?base_name file_name = module Normalized = struct type t = string + let of_string ?existence ?base_name s = normalize ?existence ?base_name s + let concat ?existence t s = normalize ?existence (t ^ s) let to_pretty_string s = pretty s let equal : t -> t -> bool = (=) let compare = String.compare diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index e1be01aac9c19146a49e688d7a0fa230efc8bf79..cce18b7d45db87db3af8590bf24f04d440cdc7d7 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -103,6 +103,10 @@ module Normalized: sig *) val of_string: ?existence:existence -> ?base_name:string -> string -> t + (** @return the normalized path resulting from the concatenation of the given + path and string. *) + val concat: ?existence:existence -> t -> string -> t + (** [to_pretty_string p] returns [p] prettified, that is, a relative path-like string. Note that this prettified string may contain symbolic dirs and is thus