From 63d293f50a0a0940c86f2080554fbe585f70a96e Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 17 Jan 2020 09:18:07 +0100
Subject: [PATCH] Add concat function for normalized filepaths.
---
src/kernel_services/plugin_entry_points/plugin.ml | 2 +-
src/libraries/datatype/datatype.ml | 1 +
src/libraries/datatype/datatype.mli | 1 +
src/libraries/utils/filepath.ml | 2 ++
src/libraries/utils/filepath.mli | 4 ++++
5 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 80fc744acfe..798d70dbf8e 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 0e55cdc83a9..417d5f8ea37 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 4243c2b50b1..9d659f95aaa 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 2a181a56473..1fc3781fcc9 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 e1be01aac9c..cce18b7d45d 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
--
GitLab