diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d50c394007b8a03fb61946d7712928981a191f3f..5adff837b78ed72fd955035ee9bcd792bba501d6 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1097,6 +1097,8 @@ src/plugins/server/kernel_main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_main.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_project.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_project.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_properties.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_properties.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 69919ab5d303fad4ab9ae6a2dfc266e5943c88ed..d5b7cf9e8dab5322982b805a00c69533c751197d 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -44,7 +44,9 @@ PLUGIN_CMO:= \
server_batch \
kernel_main \
kernel_project \
- kernel_ast
+ kernel_ast \
+ kernel_properties
+
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_TESTS_DIRS := batch
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b4d9992761e7fdc055bb7169b8d73c5b68919eaa
--- /dev/null
+++ b/src/plugins/server/kernel_properties.ml
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Sy = Syntax
+module Md = Markdown
+module Js = Yojson.Basic.Util
+
+open Data
+open Kernel_main
+open Kernel_ast
+
+(* -------------------------------------------------------------------------- *)
+(* --- Properties --- *)
+(* -------------------------------------------------------------------------- *)
+
+let page = Doc.page `Kernel ~title:"Property Services" ~filename:"properties.md"
+
+let model = States.model ()
+
+let () = States.column ~model ~name:"descr"
+ ~descr:(Md.plain "Description")
+ ~data:(module Jstring)
+ ~get:(fun ip -> Format.asprintf "%a" Property.pretty ip) ()
+
+let () = States.column ~model ~name:"status"
+ ~descr:(Md.plain "Status")
+ ~data:(module Jstring)
+ ~get:(fun ip ->
+ let st = Property_status.Feedback.get ip
+ in Format.asprintf "%a" Property_status.Feedback.pretty st) ()
+
+let () = States.column ~model ~name:"function"
+ ~descr:(Md.plain "Function")
+ ~data:(module Kf.Joption) ~get:Property.get_kf ()
+
+let () = States.column ~model ~name:"kinstr"
+ ~descr:(Md.plain "Instruction")
+ ~data:(module Ki) ~get:Property.get_kinstr ()
+
+let () = States.column ~model ~name:"source"
+ ~descr:(Md.plain "Position")
+ ~data:(module LogSource)
+ ~get:(fun ip -> Property.location ip |> fst) ()
+
+let array =
+ States.register_array
+ ~page
+ ~name:"kernel.properties"
+ ~descr:(Md.plain "Registered Properties")
+ ~key:(Property.Names.get_prop_name_id)
+ ~iter:(Property_status.iter)
+ ~add_update_hook:Property_status.register_property_add_hook
+ ~add_remove_hook:Property_status.register_property_remove_hook
+ model
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index 6b811e8a6d59b1a6d5ca952e586115fa3a8649fd..9ec13539dd1a4a1e4e83dfb3f80742f0cd7ad763 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -93,14 +93,15 @@ type 'a model = 'a column list ref
let model () = ref []
-let column (type a) (m : a model) ~name ~descr (output : a Request.output) =
- let module D = (val output) in
+let column (type a b) ~(model : a model) ~name ~descr
+ ~(data: b Request.output) ~(get : a -> b) () =
+ let module D = (val data) in
if name = "id" || name = "_index" then
raise (Invalid_argument "Server.States.column: invalid name") ;
- if List.exists (fun (fd,_) -> fd.Syntax.name = name) !m then
+ if List.exists (fun (fd,_) -> fd.Syntax.name = name) !model then
raise (Invalid_argument "Server.States.column: duplicate name") ;
let fd = Syntax.{ name ; syntax = D.syntax ; descr } in
- m := (fd , D.to_json) :: !m
+ model := (fd , fun a -> D.to_json (get a)) :: !model
module Kmap = Map.Make(String)
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
index 60f6798add7657b6db98555142cc8525a6bdcd2a..01080d8a0522afc62f7eef85aa4fa1c9885b666f 100644
--- a/src/plugins/server/states.mli
+++ b/src/plugins/server/states.mli
@@ -77,8 +77,12 @@ val model : unit -> 'a model
Columns with name `"id"` and `"_index"` are
reserved for internal use. *)
val column :
- 'a model -> name:string -> descr:Markdown.text ->
- 'a Request.output -> unit
+ model:'a model ->
+ name:string ->
+ descr:Markdown.text ->
+ data:('b Request.output) ->
+ get:('a -> 'b) ->
+ unit -> unit
type 'a array (** Synchronized array state *)