From e4e9b23672cb1b07bc4463b5d59cdbf470432f63 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 21 Mar 2022 17:14:47 +0100
Subject: [PATCH] [server] Adds optional argument [emable] to the registration
of marker information.
---
src/plugins/server/kernel_ast.ml | 18 ++++++++++--------
src/plugins/server/kernel_ast.mli | 4 +++-
2 files changed, 13 insertions(+), 9 deletions(-)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index f9fadabefdc..b3f8e006a82 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -554,6 +554,7 @@ struct
rank: int;
label: string;
title: string;
+ enable: unit -> bool;
pretty: Format.formatter -> Printer_tag.localizable -> unit
}
@@ -599,12 +600,13 @@ struct
let infos = ref [] in
Hashtbl.iter
(fun _ info ->
- match tgt with
- | None -> infos := (info, `Null) :: !infos
- | Some marker ->
- let text = jtext info.pretty marker in
- if not (Jbuffer.is_empty text) then
- infos := (info, text) :: !infos
+ if info.enable () then
+ match tgt with
+ | None -> infos := (info, `Null) :: !infos
+ | Some marker ->
+ let text = jtext info.pretty marker in
+ if not (Jbuffer.is_empty text) then
+ infos := (info, text) :: !infos
) registry ;
List.sort by_rank !infos
@@ -614,9 +616,9 @@ struct
let update () = Request.emit signal
- let register ~id ~label ~title pretty =
+ let register ~id ~label ~title ?(enable = fun _ -> true) pretty =
let rank = incr rankId ; !rankId in
- let info = { id ; rank ; label ; title ; pretty } in
+ let info = { id ; rank ; label ; title ; enable ; pretty } in
if Hashtbl.mem registry id then
( let msg = Format.sprintf
"Server.Kernel_ast.register_info: duplicate %S" id in
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 3dd3868e276..c86dd151ffc 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -73,12 +73,14 @@ sig
Identifier [id] shall be unique.
Label [label] shall be very short.
Description shall succintly describe the kind of informations.
+ If the optional [enable] function is provided, the information printer is
+ only used when [enable ()] returns true.
The printer is allowed to raise [Not_found] exception,
which is interpreted as there is no information of this kind for
the localizable.
*)
val register :
- id:string -> label:string -> title:string ->
+ id:string -> label:string -> title:string -> ?enable:(unit -> bool) ->
(Format.formatter -> Printer_tag.localizable -> unit) -> unit
(** Updated informations signal *)
--
GitLab