[server] Adds a synchronized array of emitted messages.

ivette/src/frama-c/api/generated/kernel/services/index.ts

@@ -150,6 +150,99 @@ const logkindTags_internal: Server.GetRequest<null,tag[]> = {
 /** Registered tags for the above type. */
 export const logkindTags: Server.GetRequest<null,tag[]>= logkindTags_internal;
 
+/** Data for array rows [`message`](#message)  */
+export interface messageData {
+  /** Entry identifier. */
+  key: Json.key<'#message'>;
+  /** Message kind */
+  kind: logkind;
+  /** Emitter plugin */
+  plugin: string;
+  /** Message text */
+  message: string;
+  /** Message category (only for debug or warning messages) */
+  category?: string;
+  /** Source file position */
+  source?: source;
+}
+
+/** Loose decoder for `messageData` */
+export const jMessageData: Json.Loose<messageData> =
+  Json.jObject({
+    key: Json.jFail(Json.jKey<'#message'>('#message'),'#message expected'),
+    kind: jLogkindSafe,
+    plugin: Json.jFail(Json.jString,'String expected'),
+    message: Json.jFail(Json.jString,'String expected'),
+    category: Json.jString,
+    source: jSource,
+  });
+
+/** Safe decoder for `messageData` */
+export const jMessageDataSafe: Json.Safe<messageData> =
+  Json.jFail(jMessageData,'MessageData expected');
+
+/** Natural order for `messageData` */
+export const byMessageData: Compare.Order<messageData> =
+  Compare.byFields
+    <{ key: Json.key<'#message'>, kind: logkind, plugin: string,
+       message: string, category?: string, source?: source }>({
+    key: Compare.string,
+    kind: byLogkind,
+    plugin: Compare.alpha,
+    message: Compare.string,
+    category: Compare.defined(Compare.string),
+    source: Compare.defined(bySource),
+  });
+
+/** Signal for array [`message`](#message)  */
+export const signalMessage: Server.Signal = {
+  name: 'kernel.services.signalMessage',
+};
+
+const reloadMessage_internal: Server.GetRequest<null,null> = {
+  kind: Server.RqKind.GET,
+  name:   'kernel.services.reloadMessage',
+  input:  Json.jNull,
+  output: Json.jNull,
+  signals: [],
+};
+/** Force full reload for array [`message`](#message)  */
+export const reloadMessage: Server.GetRequest<null,null>= reloadMessage_internal;
+
+const fetchMessage_internal: Server.GetRequest<
+  number,
+  { pending: number, updated: messageData[], removed: Json.key<'#message'>[],
+    reload: boolean }
+  > = {
+  kind: Server.RqKind.GET,
+  name:   'kernel.services.fetchMessage',
+  input:  Json.jNumber,
+  output: Json.jObject({
+            pending: Json.jFail(Json.jNumber,'Number expected'),
+            updated: Json.jList(jMessageData),
+            removed: Json.jList(Json.jKey<'#message'>('#message')),
+            reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+          }),
+  signals: [],
+};
+/** Data fetcher for array [`message`](#message)  */
+export const fetchMessage: Server.GetRequest<
+  number,
+  { pending: number, updated: messageData[], removed: Json.key<'#message'>[],
+    reload: boolean }
+  >= fetchMessage_internal;
+
+const message_internal: State.Array<Json.key<'#message'>,messageData> = {
+  name: 'kernel.services.message',
+  getkey: ((d:messageData) => d.key),
+  signal: signalMessage,
+  fetch: fetchMessage,
+  reload: reloadMessage,
+  order: byMessageData,
+};
+/** Log messages */
+export const message: State.Array<Json.key<'#message'>,messageData> = message_internal;
+
 /** Message event record. */
 export interface log {
   /** Message kind */

src/plugins/server/kernel_main.ml

@@ -166,6 +166,49 @@ struct
   include (val data : S with type t = Log.kind)
 end
 
+(* -------------------------------------------------------------------------- *)
+(* --- Synchronized array of log events                                   --- *)
+(* -------------------------------------------------------------------------- *)
+
+let model = States.model ()
+
+let () = States.column model ~name:"kind"
+    ~descr:(Md.plain "Message kind")
+    ~data:(module LogKind)
+    ~get:(fun (evt, _) -> evt.Log.evt_kind)
+
+let () = States.column model ~name:"plugin"
+    ~descr:(Md.plain "Emitter plugin")
+    ~data:(module Jalpha)
+    ~get:(fun (evt, _) -> evt.Log.evt_plugin)
+
+let () = States.column model ~name:"message"
+    ~descr:(Md.plain "Message text")
+    ~data:(module Jstring)
+    ~get:(fun (evt, _) -> evt.Log.evt_message)
+
+let () = States.option model ~name:"category"
+    ~descr:(Md.plain "Message category (only for debug or warning messages)")
+    ~data:(module Jstring)
+    ~get:(fun (evt, _) -> evt.Log.evt_category)
+
+let () = States.option model ~name:"source"
+    ~descr:(Md.plain "Source file position")
+    ~data:(module LogSource)
+    ~get:(fun (evt, _) -> evt.Log.evt_source)
+
+let iter f = ignore (Messages.fold (fun i evt -> f (evt, i); succ i) 0)
+
+let _array =
+  States.register_array
+    ~package
+    ~name:"message"
+    ~descr:(Md.plain "Log messages")
+    ~key:(fun (_evt, i) -> string_of_int i)
+    ~iter:iter
+    ~add_reload_hook:Messages.add_global_hook
+    model
+
 (* -------------------------------------------------------------------------- *)
 (* --- Log Events                                                         --- *)
 (* -------------------------------------------------------------------------- *)