diff --git a/.Makefile.lint b/.Makefile.lint
index 45b0947948bf34583b88506bce3b0b8c9fc134d0..c50a31c64446d42a9580f22d45c7b17d615968fe 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -104,8 +104,6 @@ ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.mli
ML_LINT_KO+=src/kernel_services/parsetree/logic_ptree.mli
ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/dynamic.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/dynamic.mli
ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.mli
ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 56af09583638176d86d5f470bf9bd1edb4546c61..160d39bcf4743e2bb176574380d78f7539e9ac63 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -55,24 +55,24 @@ exception Unbound_value = Tbl.Unbound_value
let dynlib_error name = function
| Dynlink.Error e ->
- error ~name ~message:"cannot load module" ~details:(Dynlink.error_message e) ;
+ error ~name ~message:"cannot load module" ~details:(Dynlink.error_message e) ;
| Sys_error _ as e ->
- error ~name ~message:"system error" ~details:(Printexc.to_string e)
+ error ~name ~message:"system error" ~details:(Printexc.to_string e)
| Unloadable details ->
- error ~name ~message:"incompatible with current set-up" ~details
+ error ~name ~message:"incompatible with current set-up" ~details
(* the three next errors may be raised in case of incompatibilities with
another plug-in *)
| Incompatible_type s ->
- error ~name ~message:"code incompatibility" ~details:s
+ error ~name ~message:"code incompatibility" ~details:s
| Unbound_value s ->
- error ~name ~message:"code incompatibility" ~details:("unbound value " ^ s)
+ error ~name ~message:"code incompatibility" ~details:("unbound value " ^ s)
| Type.No_abstract_type s ->
- error ~name ~message:"code incompatibility" ~details:("unbound abstract type " ^ s)
+ error ~name ~message:"code incompatibility" ~details:("unbound abstract type " ^ s)
| Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- raise e
+ raise e
| e ->
- error ~name ~message:("unexpected exception: " ^ Printexc.to_string e)
- ~details:(Printexc.get_backtrace ())
+ error ~name ~message:("unexpected exception: " ^ Printexc.to_string e)
+ ~details:(Printexc.get_backtrace ())
let dynlib_module name file =
Klog.feedback ~dkey "Loading module '%s' from '%s'." name file ;
@@ -244,7 +244,8 @@ let load_script base =
Format.fprintf fmt "%s -shared -o %S.cmxs" Fc_config.ocamlopt base
else
Format.fprintf fmt "%s -c" Fc_config.ocamlc ;
- Format.fprintf fmt " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
+ Format.fprintf fmt
+ " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
if !Fc_config.is_gui && Fc_config.lablgtk <> "" then
Format.fprintf fmt " -package %s" Fc_config.lablgtk;
List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
@@ -322,31 +323,31 @@ let load_module m =
let base,ext = split_ext m in
match ext with
| ".ml" ->
- begin
- (* force script compilation *)
+ begin
+ (* force script compilation *)
+ match is_file base ".ml" with
+ | Some _ -> load_script base
+ | None -> Klog.error "Missing source file '%s'" m
+ end
+ | "" | "." | ".cmo" | ".cma" | ".cmxs" ->
+ begin
+ (* load object or compile script or find package *)
+ match is_object base with
+ | Some file -> dynlib_module (Filename.basename base) file
+ | None ->
match is_file base ".ml" with
| Some _ -> load_script base
- | None -> Klog.error "Missing source file '%s'" m
- end
- | "" | "." | ".cmo" | ".cma" | ".cmxs" ->
- begin
- (* load object or compile script or find package *)
- match is_object base with
- | Some file -> dynlib_module (Filename.basename base) file
| None ->
- match is_file base ".ml" with
- | Some _ -> load_script base
- | None ->
- if is_package m && mem_package m then load_packages [m]
- else
- let fc =
- "frama-c-" ^ String.lowercase_ascii m
- in
- if mem_package fc then load_packages [fc]
- else Klog.error "package or module '%s' not found" m
- end
+ if is_package m && mem_package m then load_packages [m]
+ else
+ let fc =
+ "frama-c-" ^ String.lowercase_ascii m
+ in
+ if mem_package fc then load_packages [fc]
+ else Klog.error "package or module '%s' not found" m
+ end
| _ ->
- Klog.error "don't know what to do with '%s' (unexpected %s)" m ext
+ Klog.error "don't know what to do with '%s' (unexpected %s)" m ext
(* ************************************************************************* *)
(** {2 Registering and accessing dynamic values} *)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index 79a789e0e45983ea87547ae49ac13eb310837550..cf663dc88ff45bfbb3b31aee709d84a8727869c3 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -28,8 +28,8 @@
(* ************************************************************************* *)
val register:
- ?comment:string ->
- plugin:string ->
+ ?comment:string ->
+ plugin:string ->
string -> 'a Type.t -> journalize:bool -> 'a -> 'a
(** [register ~plugin name ty v] registers [v] with the name
[name], the type [ty] and the plug-in [plugin].
@@ -71,7 +71,7 @@ val iter_comment : (string -> string -> unit) -> unit
(* ************************************************************************* *)
(** Module to use for accessing parameters of plug-ins.
- Assume that the plug-in is already loaded.
+ Assume that the plug-in is already loaded.
@plugin development guide *)
module Parameter : sig
@@ -99,7 +99,7 @@ module Parameter : sig
(** Not for casual users *)
(**/**)
- (** Boolean parameters.
+ (** Boolean parameters.
@plugin development guide *)
module Bool: sig
include Common with type t = bool