From 3a05a5fe76ba94d1f0f9f74ad5014eaff5c90449 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 18 Sep 2024 14:39:44 +0200
Subject: [PATCH] [doc] Update documentation for dkeys/wkeys
---
doc/developer/advance.tex | 37 ++++++++++---------
.../plugin_entry_points/log.mli | 8 +++-
2 files changed, 26 insertions(+), 19 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6474f804b2..9aee2607d8 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1337,13 +1337,14 @@ debugging level is used.
output can be associated to a debugging key with the optional argument
\lstinline{~dkey} which takes an argument of abstract type
\lstinline|category|.
-Each category must be registered through the
-\lstinline|register_category| function. You can define subcategories
-by putting colons in the registered name. For instance \lstinline|a:b:c| defines
-a subcategory \lstinline|c| of \lstinline|a:b|, itself a subcategory of
-\lstinline|a|. User can then choose to
-output debugging messages belonging to a given category (and its subcategories)
-with the \lstinline{-plugin-msg-key <category>} option.
+Each category must be registered through the \lstinline|register_category|
+function which takes an optionnal parameter \lstinline|help| to provide a
+short description for this category. You can define subcategories by putting
+colons in the registered name. For instance \lstinline|a:b:c| defines a
+subcategory \lstinline|c| of \lstinline|a:b|, itself a subcategory of
+\lstinline|a|. User can then choose to output debugging messages belonging to a
+given category (and its subcategories) with the
+\lstinline{-plugin-msg-key <category>} option.
In order to decide whether a message should be output, both level and category
options are examined:
@@ -1364,18 +1365,18 @@ options are examined:
what they want to see on the output.
\end{itemize}
-\paragraph{Warning Category Option} Warning output can also
-be associated with a category, via the \lstinline|~wkey| optional argument
-that takes a value of abstract type
-\sscodeidxdef{Log}{Messages}{warn\_category}
-\lstinline|warn_category|. Warning categories
-are distinct from plain categories, and must be registered with the
+\paragraph{Warning Category Option} Warning output can also be associated with a
+category, via the \lstinline|~wkey| optional argument that takes a value of
+abstract type \sscodeidxdef{Log}{Messages}{warn\_category}
+\lstinline|warn_category|. Warning categories are distinct from plain
+categories, and must be registered with the
\sscodeidxdef{Log}{Messages}{register\_warn\_category}
-\lstinline|register_warn_category| function. As explained in the user
-manual~\cite{userman}, each category can be associated with a status that
-controls what will happen when a warning is triggered, from completely ignoring
-it to aborting execution. The default is to emit the warning, but this can
-be changed by using the
+\lstinline|register_warn_category| function which takes an optionnal parameter
+\lstinline|help| to provide a short description for this warning category. As
+explained in the user manual~\cite{userman}, each category can be associated
+with a status that controls what will happen when a warning is triggered, from
+completely ignoring it to aborting execution. The default is to emit the
+warning, but this can be changed by using the
\sscodeidxdef{Log}{Messages}{set\_warn\_status}
\lstinline|set_warn_status| function.
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 711ce21250..5f04999714 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -283,6 +283,7 @@ module type Messages = sig
Note: to enable a category's messages by default, add it
(e.g. via [add_debug_keys]) after registration.
@since Fluorine-20130401
+ @before Frama-C+dev [?help] option was not present
*)
val pp_category: Format.formatter -> category -> unit
@@ -291,6 +292,9 @@ module type Messages = sig
*)
val pp_all_categories: unit -> unit
+ (** pretty-prints all categories.
+ @since Frama-C+dev
+ *)
val dkey_name: category -> string
(** returns the category name as a string.
@@ -338,7 +342,9 @@ module type Messages = sig
*)
val register_warn_category: ?help:string -> string -> warn_category
- (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+ @before Frama-C+dev [?help] option was not present
+ *)
val is_warn_category: string -> bool
--
GitLab