diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index fbad1cab3272dcb7bec80b992711f55f945b4461..80881489f15e2a298c73e0f316f432f1a9c5ec6b 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 2a6a18e92cd0c0f1a41585c7caae9707f74b2fb5..456dae219a15c6f38969ed908b003ba67619ccc8 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 d26971988256225f5b5f98a82bfb2a7bba4286ee..49e2f1433d6c778fb4c6d10de01a67bb6eb23032 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 92429eec2cb1a28388d784e9da503c02c408f12c..581fe62fbf8756b730889f4167bb9310c834851d 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 35117db7c005009230504c8fe0144a386d60b469..28fafe6d94b701c16f25e1b9cf7d4f0daa9bcc3f 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 d60942fa9c8e7be7beaa6ee422e3cb95e1c92f87..2556a163b6e7abaaa7565b3d108adb4b6e5975e2 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 cb3f72b73511c3c05d29f827e0f63eb9de2a7933..a02122eaa141ba335726ccd72c76267f023e2bd4 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 49568f9c4f0eac68c17ce3bcae6eb9fbf04d96f5..39798e3efef3bb17f497d9ef1ff1a7da81101dd9 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 93505053884d755ef47f144217477f9e8cb76b33..447e7ae8e0a669303dfd0273ca5a7cdac9b44783 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