From 1f3fc9c662feab2a8f8b08cc0163d2b50764d352 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 16 Sep 2020 21:37:13 +0200
Subject: [PATCH] [Kernel] replace do_iterate with is_reconfigurable
Allows iterating through _all_ plugin options, while keeping same list of
options for the GUI.
Typed parameters have two extra fields:
- visible: must be synchronized with the Cmdline.visible field;
- reconfigurable: to be shown in the GUI's "Analyses" panel.
iter_on_plugins (and fold_on_plugins) operate over all plugin options
---
.../cmdline_parameters/parameter_builder.ml | 40 +++++++++++--------
.../cmdline_parameters/parameter_customize.ml | 10 ++---
.../parameter_customize.mli | 25 +++++++-----
.../cmdline_parameters/typed_parameter.ml | 10 +++--
.../cmdline_parameters/typed_parameter.mli | 4 ++
.../plugin_entry_points/kernel.ml | 11 +++--
.../plugin_entry_points/plugin.ml | 4 +-
.../plugin_entry_points/plugin.mli | 7 ++--
src/plugins/gui/launcher.ml | 5 ++-
9 files changed, 69 insertions(+), 47 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index fbad1cab327..80881489f15 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -70,8 +70,8 @@ let force_ast_compute
(** {2 Specific functors} *)
(* ************************************************************************* *)
-let iter_on_this_parameter stage =
- match !Parameter_customize.do_iterate_ref, stage with
+let is_parameter_reconfigurable stage =
+ match !Parameter_customize.is_reconfigurable_ref, stage with
| Some false, _
| None, (Cmdline.Early | Cmdline.Extending | Cmdline.Extended
| Cmdline.Exiting | Cmdline.Loading) ->
@@ -96,17 +96,15 @@ struct
let parameters_ref : Typed_parameter.t list ref = ref []
let parameters () = !parameters_ref
- let add_parameter group stage param =
- if iter_on_this_parameter stage then begin
- parameters_ref := param :: !parameters_ref;
- let parameter_groups = P.parameters in
- try
- let group_name = Cmdline.Group.name group in
- let parameters = Hashtbl.find P.parameters group_name in
- Hashtbl.replace parameter_groups group_name (param :: parameters)
- with Not_found ->
- assert false
- end
+ let add_parameter group _stage param =
+ parameters_ref := param :: !parameters_ref;
+ let parameter_groups = P.parameters in
+ try
+ let group_name = Cmdline.Group.name group in
+ let parameters = Hashtbl.find P.parameters group_name in
+ Hashtbl.replace parameter_groups group_name (param :: parameters)
+ with Not_found ->
+ assert false
(* ************************************************************************ *)
(** {3 Bool} *)
@@ -212,8 +210,10 @@ struct
add_set_hook = add_set_hook; add_update_hook = add_update_hook },
negative_option)
in
+ let reconfigurable = is_parameter_reconfigurable stage in
let p =
- Typed_parameter.create ~name ~help:X.help ~accessor:accessor ~is_set
+ Typed_parameter.create ~name ~help:X.help ~accessor:accessor
+ ~visible:is_visible ~reconfigurable ~is_set
in
add_parameter !Parameter_customize.group_ref stage p;
Parameter_customize.reset ();
@@ -318,8 +318,10 @@ struct
add_set_hook = add_set_hook; add_update_hook = add_update_hook },
get_range)
in
+ let reconfigurable = is_parameter_reconfigurable stage in
let p =
- Typed_parameter.create ~name ~help:X.help ~accessor ~is_set:is_set
+ Typed_parameter.create ~name ~help:X.help ~accessor
+ ~visible:is_visible ~reconfigurable ~is_set:is_set
in
add_parameter !Parameter_customize.group_ref stage p;
add_option X.option_name;
@@ -425,8 +427,10 @@ struct
add_set_hook = add_set_hook; add_update_hook = add_update_hook },
get_possible_values)
in
+ let reconfigurable = is_parameter_reconfigurable stage in
let p =
- Typed_parameter.create ~name ~help:X.help ~accessor ~is_set
+ Typed_parameter.create ~name ~help:X.help ~accessor
+ ~visible:is_visible ~reconfigurable ~is_set
in
add_parameter !Parameter_customize.group_ref stage p;
add_option X.option_name;
@@ -513,8 +517,10 @@ struct
add_update_hook = parameter_add_update_hook },
fun () -> [])
in
+ let reconfigurable = is_parameter_reconfigurable stage in
let p =
- Typed_parameter.create ~name ~help:X.help ~accessor ~is_set
+ Typed_parameter.create ~name ~help:X.help ~accessor
+ ~visible:is_visible ~reconfigurable ~is_set
in
add_parameter !Parameter_customize.group_ref stage p;
add_option X.option_name;
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.ml b/src/kernel_services/cmdline_parameters/parameter_customize.ml
index 2a6a18e92cd..456dae219a1 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.ml
@@ -81,14 +81,14 @@ let argument_must_be_existing_fun () =
let group_ref = ref Cmdline.Group.default
let set_group s = group_ref := s
-let do_iterate_ref = ref None
-let do_iterate () = do_iterate_ref := Some true
-let do_not_iterate () = do_iterate_ref := Some false
+let is_reconfigurable_ref = ref None
+let is_reconfigurable () = is_reconfigurable_ref := Some true
+let is_not_reconfigurable () = is_reconfigurable_ref := Some false
let is_visible_ref = ref true
let is_invisible () =
is_visible_ref := false;
- do_not_iterate ()
+ is_not_reconfigurable ()
let use_category_ref = ref true
let no_category () = use_category_ref := false
@@ -124,7 +124,7 @@ let reset () =
must_save_ref := true;
module_name_ref := empty_string;
group_ref := Cmdline.Group.default;
- do_iterate_ref := None;
+ is_reconfigurable_ref := None;
is_visible_ref := true;
argument_is_function_name_ref := false;
argument_may_be_fundecl_ref := false;
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index d2697198825..49e2f1433d6 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -90,7 +90,8 @@ val set_group: Cmdline.Group.t -> unit
@since Beryllium-20090901 *)
val is_invisible: unit -> unit
-(** Prevent the help to list the parameter. Also imply {!do_not_iterate}.
+(** Prevent -help from listing the parameter.
+ Also imply {!is_not_reconfigurable}.
@since Carbon-20101201
@modify Nitrogen-20111001 does not appear in the help *)
@@ -123,17 +124,21 @@ val argument_must_be_existing_fun: unit -> unit
unset, names of defined-only functions will raise an error as well.
@since Sodium-20150201 *)
-val do_iterate: unit -> unit
-(** Ensure that {!iter_on_plugins} is applied to this parameter. By default
+val is_reconfigurable: unit -> unit
+(** Ensure that the GUI will show this parameter. By default
only parameters corresponding to options registered at the
- {!Cmdline.Configuring} stage are iterable.
- @since Nitrogen-20111001 *)
+ {!Cmdline.Configuring} stage are reconfigurable.
+ @since Nitrogen-20111001
+ @modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable]
+*)
-val do_not_iterate: unit -> unit
-(** Prevent {!iter_on_plugins} to be applied on the parameter. By default, only
+val is_not_reconfigurable: unit -> unit
+(** Prevent the GUI from showing this parameter. By default, only
parameters corresponding to options registered at the
- {!Cmdline.Configuring} stage are iterable.
- @since Nitrogen-20111001 *)
+ {!Cmdline.Configuring} stage are reconfigurable.
+ @since Nitrogen-20111001
+ @modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable]
+ *)
val no_category: unit -> unit
(** Prevent a collection parameter to use categories and the extension '+', and
@@ -206,7 +211,7 @@ val argument_may_be_fundecl_ref: bool ref
val argument_must_be_fundecl_ref: bool ref
val argument_must_be_existing_fun_ref: bool ref
val group_ref: Cmdline.Group.t ref
-val do_iterate_ref: bool option ref
+val is_reconfigurable_ref: bool option ref
val is_visible_ref: bool ref
val module_name_ref: string ref
val use_category_ref: bool ref
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.ml b/src/kernel_services/cmdline_parameters/typed_parameter.ml
index 92429eec2cb..581fe62fbf8 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.ml
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.ml
@@ -36,7 +36,9 @@ type typed_accessor =
type parameter =
{ name: string;
help: string;
- accessor: typed_accessor;
+ accessor: typed_accessor;
+ visible: bool;
+ reconfigurable: bool;
is_set: unit -> bool }
include
@@ -56,6 +58,8 @@ include
add_set_hook = (fun _ -> ());
add_update_hook = (fun _ -> ()) },
None);
+ visible = false ;
+ reconfigurable = false ;
is_set = fun () -> false }
]
let equal = (==)
@@ -71,8 +75,8 @@ include
let parameters = Datatype.String.Hashtbl.create 97
-let create ~name ~help ~accessor ~is_set =
- let p = { name = name; help = help; accessor = accessor; is_set = is_set } in
+let create ~name ~help ~accessor ~visible ~reconfigurable ~is_set =
+ let p = { name; help; accessor; visible; reconfigurable; is_set } in
(* parameter name unicity already checks in [Plugin]. *)
assert (not (Datatype.String.Hashtbl.mem parameters name));
Datatype.String.Hashtbl.add parameters name p;
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.mli b/src/kernel_services/cmdline_parameters/typed_parameter.mli
index 35117db7c00..28fafe6d94b 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.mli
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.mli
@@ -45,6 +45,8 @@ type parameter = private
help: string; (** Help message *)
accessor: typed_accessor; (** How to get and set the value of the
parameter *)
+ visible: bool; (** Is visible to the user, e.g. in the command-line help *)
+ reconfigurable: bool; (** Can be reconfigured, e.g. in the GUI *)
is_set: unit -> bool (** Is this option really set? *) }
include Datatype.S_with_collections with type t = parameter
@@ -61,6 +63,8 @@ val create:
name:string ->
help:string ->
accessor:typed_accessor ->
+ visible:bool ->
+ reconfigurable:bool ->
is_set: (unit -> bool) ->
t
(**/**)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d60942fa9c8..2556a163b6e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -424,11 +424,10 @@ module AutocompleteHelp =
P.String_set
(struct
let option_name = "-autocomplete"
- let arg_name = "[+]p1,p2,..."
+ let arg_name = "p1,p2,..."
let help = "displays all Frama-C options, used for shell autocompletion. \
Prints options for the specified plugin names (or '@all' for \
- all plugins). If the first character is '+', \
- only prints visible options."
+ all plugins). Note: for the kernel, use an empty string."
end)
let _ =
@@ -471,7 +470,7 @@ let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
-let () = Parameter_customize.do_iterate ()
+let () = Parameter_customize.is_reconfigurable ()
module GeneralVerbose =
Int
(struct
@@ -493,7 +492,7 @@ let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
-let () = Parameter_customize.do_iterate ()
+let () = Parameter_customize.is_reconfigurable ()
module GeneralDebug =
Zero
(struct
@@ -517,7 +516,7 @@ let () =
let () = Parameter_customize.set_group messages
let () = Parameter_customize.set_negative_option_name ""
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
-let () = Parameter_customize.do_iterate ()
+let () = Parameter_customize.is_reconfigurable ()
let () = Parameter_customize.do_not_projectify ()
let () = Parameter_customize.do_not_journalize ()
module Quiet =
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index cb3f72b7351..a02122eaa14 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -311,7 +311,7 @@ struct
let () =
Parameter_customize.set_cmdline_stage Cmdline.Extended;
- if is_visible then Parameter_customize.do_iterate ()
+ if is_visible then Parameter_customize.is_reconfigurable ()
else Parameter_customize.is_invisible ()
module Dir_name =
@@ -517,7 +517,7 @@ struct
Parameter_customize.set_group messages;
Parameter_customize.do_not_projectify ();
Parameter_customize.do_not_journalize ();
- Parameter_customize.do_iterate ();
+ Parameter_customize.is_reconfigurable ();
if is_kernel () then begin
Parameter_customize.set_cmdline_stage Cmdline.Early;
Parameter_customize.set_module_name modname;
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 49568f9c4f0..39798e3efef 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -89,9 +89,10 @@ type plugin = private
p_shortname: string;
p_help: string;
p_parameters: (string, Typed_parameter.t list) Hashtbl.t }
-(** Only iterable parameters (see {!do_iterate} and {!do_not_iterate}) are
- registered in the field [p_parameters].
- @since Beryllium-20090901 *)
+(** @since Beryllium-20090901
+ @modify Frama-C+dev previously only "iterable" parameters were included,
+ now all parameters are.
+*)
module type General_services = sig
include S
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index 93505053884..447e7ae8e0a 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -137,7 +137,10 @@ let add_group (box:GPack.box) label options =
in
let highlight =
List.fold_right
- (fun p b -> let is_set = add_parameter box p in b || is_set)
+ (fun p b ->
+ if p.Typed_parameter.reconfigurable then
+ let is_set = add_parameter box p in b || is_set
+ else b)
options
false
in
--
GitLab