From 0ecf30a0d38306f6b259bdb85b9713ae25101d26 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 22 Apr 2020 15:07:41 +0200
Subject: [PATCH] [kernel] Some comments.
---
.../cmdline_parameters/parameter_sig.mli | 21 +++++++++++++++++++
.../plugin_entry_points/plugin.ml | 7 ++++++-
2 files changed, 27 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 4906addb827..2dd81a0d804 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -296,18 +296,39 @@ module type Filepath = S with type t = Filepath.Normalized.t
module type Specific_dir = sig
val set: Filepath.Normalized.t -> unit
+ (** Sets the plugin <specific-dir> directory (without creating it). *)
+
val get: unit -> Filepath.Normalized.t
+ (** @return the plugin <specific-dir> directory (without creating it). *)
+
val is_set: unit -> bool
+ (** @return whether the plugin <specific-dir> has been set. *)
val get_dir:
?mode:[`Create_path | `Normalize_only | `Must_exist ] ->
string ->
Filepath.Normalized.t
+ (**[get_dir ?mode p] returns a local-path [p], relative to the plugin
+ <specific-dir> directory, to a sub-directory of the plugin <specific-dir>
+ directory.
+ @param mode determines how to handle the resulting path:
+ + [Create_path] creates the resulting path, if does not exist.
+ + [Normalize_only] just normalizes the resulting path.
+ + [Must_exist] aborts if the resulting path does not exist.
+ *)
val get_file:
?mode:[`Create_path | `Normalize_only | `Must_exist ] ->
string ->
Filepath.Normalized.t
+ (**[get_file ?mode p] returns a local-path [p], relative to the plugin
+ <specific-dir> directory, to a file in the plugin <specific-dir>
+ directory.
+ @param mode determines how to handle the resulting path:
+ + [Create_path] creates the dirname of resulting path, if does not exist.
+ + [Normalize_only] just normalizes the resulting path.
+ + [Must_exist] aborts if the resulting path does not exist.
+ *)
end
(* ************************************************************************** *)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index ecc78065fc3..3e4c529f2b6 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -343,7 +343,8 @@ struct
if not (plugin_base_dir = Datatype.Filepath.dummy)
then [plugin_base_dir]
else begin
- (* No specified dir: look for the default one. *)
+ (* No specified dir: look for the default ones.
+ At least one default value must be in place. *)
let dirs = D.dirs () in
assert (dirs <> []);
if is_kernel
@@ -380,6 +381,8 @@ struct
end
| _ ->
begin
+ (* In presence of more than one base directory, consider the first to
+ form the resulting [filepath]. *)
let filepath =
match base_dirs () with
| [] -> assert false
@@ -409,6 +412,8 @@ struct
| `Normalize_only ->
filepath
| `Create_path ->
+ (* No need to create anything here, as the path of sub-directories has
+ been already created by [get_dir] for computing [base_dir]. *)
filepath
end
--
GitLab