From 7cbc7b4a18200c6e893ea0fcddde21000dd812d2 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Jan 2021 16:54:29 +0100
Subject: [PATCH] [kernel] allow -add-symbolic-path to survive saves/loads
---
.../plugin_entry_points/kernel.ml | 62 +++++++++++--------
.../plugin_entry_points/kernel.mli | 5 +-
src/libraries/utils/filepath.ml | 2 +
src/libraries/utils/filepath.mli | 4 ++
4 files changed, 45 insertions(+), 28 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 27e2b1cd3fe..9bbf197ec1e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -24,7 +24,6 @@
(** {2 Kernel as an almost standard plug-in} *)
(* ************************************************************************* *)
-module CamlString = String
module FcPlugin = Plugin
let () = Plugin.register_kernel ()
@@ -251,13 +250,6 @@ module String
include X
end)
-module String_set(X: Input_with_arg) =
- P.String_set
- (struct
- let () = Parameter_customize.set_module_name X.module_name
- include X
- end)
-
module String_list(X: Input_with_arg) =
P.String_list
(struct
@@ -606,16 +598,50 @@ module Time =
let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
module SymbolicPath =
- String_set (* TODO: to be replaced by an hashtbl *)
+ Filepath_map
(struct
let option_name = "-add-symbolic-path"
let module_name = "SymbolicPath"
let arg_name = "name_1:path_1,...,name_n:path_n"
+ let existence = Filepath.Indifferent
+ let file_kind = "directory"
let help =
- "When displaying file locations, replace (absolute) path by the \
+ "When displaying file locations, replace (absolute) path with the \
corresponding symbolic name"
end)
+let () =
+ SymbolicPath.add_update_hook
+ (fun _ map ->
+ (* keep module [Filepath] synchronized with [SymbolicPath] *)
+ Filepath.reset_symbolic_dirs ();
+ Datatype.Filepath.Map.iter
+ (fun n p -> Filepath.add_symbolic_dir p (n :> string))
+ map)
+
+(* [SymbolicPath] is better to be not projectified,
+ but must be saved: use a fake state for saving it without projectifying it *)
+module SymbolicPathFakeState =
+ State_builder.Register
+ (Datatype.Unit)
+ (struct
+ type t = unit
+ let create () = ()
+ let clear _ = ()
+ let get () = ()
+ let set () = ()
+ let clear_some_projects _ _ = false
+ end)
+ (struct
+ let name = "SymbolicPathFakeState"
+ let unique_name = name
+ let dependencies = []
+ end)
+
+let () =
+ SymbolicPathFakeState.howto_marshal
+ (fun () -> SymbolicPath.get ())
+ (fun paths -> SymbolicPath.set paths)
(* ************************************************************************* *)
(** {2 Input / Output Source Code} *)
@@ -712,22 +738,6 @@ module CodeOutput = struct
end
-let add_path s =
- try
- let n = CamlString.index s ':' in
- let name = CamlString.sub s 0 n in
- let path = CamlString.sub s (n+1) (CamlString.length s - (n+1)) in
- Filepath.add_symbolic_dir name path
- with Not_found ->
- warning "%s is not a valid option argument for -add-symbolic-path. \
- It will be ignored" s
-
-let () =
- SymbolicPath.add_set_hook
- (fun o n ->
- let d = Datatype.String.Set.diff n o in
- Datatype.String.Set.iter add_path d)
-
let () = Parameter_customize.set_group inout_source
let () = Parameter_customize.do_not_projectify ()
module FloatNormal =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c6ffe271274..b569b2db596 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -306,8 +306,9 @@ module CodeOutput : sig
end
(** Behavior of option "-add-symbolic-path"
- @since Neon-20140301 *)
-module SymbolicPath: Parameter_sig.String_set
+ @since Neon-20140301
+ @modify Frama-C+dev inversed argument order (now uses path:name) *)
+module SymbolicPath: Parameter_sig.Filepath_map
module FloatNormal: Parameter_sig.Bool
(** Behavior of option "-float-normal" *)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 76e2b687498..0d710ddc909 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -173,6 +173,8 @@ let add_symbolic_dir name dir =
Hashtbl.replace symbolic_dirs name dir;
(insert cwd dir).symbolic_name <- Some name
+let reset_symbolic_dirs () = Hashtbl.clear symbolic_dirs
+
let rec add_uri_path buffer path =
let open Buffer in
match path.symbolic_name with
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 79a3d7fad11..346e3c3fc15 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -89,6 +89,10 @@ val pretty: string -> string
printed identically in different machines. *)
val add_symbolic_dir: string -> string -> unit
+(** Remove all symbolic dirs that have been added earlier.
+ @since Frama-C+dev *)
+val reset_symbolic_dirs: unit -> unit
+
(** Returns the list of symbolic dirs added via [add_symbolic_dir], plus
preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir).
--
GitLab