diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in index 48b3e23e469e7fa3aeb5903b08f38543e0cecdff..8ea6491e50333f7a094429ae7b90df01e18bec97 100644 --- a/src/plugins/server/Makefile.in +++ b/src/plugins/server/Makefile.in @@ -39,7 +39,8 @@ PLUGIN_NAME:=Server PLUGIN_CMO:= \ server_parameters \ jbuffer \ - doc syntax data main request \ + doc syntax data \ + main request states \ server_batch \ kernel_main \ kernel_project \ diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml new file mode 100644 index 0000000000000000000000000000000000000000..f3af381df65192e3ea920fbbc0e9a87311c81c9a --- /dev/null +++ b/src/plugins/server/states.ml @@ -0,0 +1,58 @@ +(**************************************************************************) +(* *) +(* 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). *) +(* *) +(**************************************************************************) + +(* -------------------------------------------------------------------------- *) +(* --- Values & States --- *) +(* -------------------------------------------------------------------------- *) + +let register_value (type a) ~page ~name ~descr ?(details=[]) + ~(output : a Request.output) ~get = + let open Markdown in + let title = Printf.sprintf "`VALUE` %s" name in + let index = [ Printf.sprintf "%s (`VALUE`)" name ] in + let description = [ Block [Text descr] ; Block details] in + let h = Doc.publish ~page ~name ~title ~index description [] in + let signal = Request.signal ~page ~name:(name ^ ".sig") + ~descr:(plain "Signal for value " @ href h) () in + Request.register ~page ~kind:`GET ~name:(name ^ ".get") + ~descr:(plain "Getter for value " @ href h) + ~input:(module Data.Junit) ~output get ; + signal + +let register_state (type a) ~page ~name ~descr ?(details=[]) + ~(data : a Data.data) ~get ~set = + let open Markdown in + let title = Printf.sprintf "`STATE` %s" name in + let index = [ Printf.sprintf "%s (`STATE`)" name ] in + let description = [ Block [Text descr] ; Block details] in + let h = Doc.publish ~page ~name ~title ~index description [] in + let signal = Request.signal ~page ~name:(name ^ ".sig") + ~descr:(plain "Signal for state " @ href h) () in + Request.register ~page ~kind:`GET ~name:(name ^ ".get") + ~descr:(plain "Getter for state " @ href h) + ~input:(module Data.Junit) ~output:(module (val data)) get ; + Request.register ~page ~kind:`SET ~name:(name ^ ".set") + ~descr:(plain "Setter for state " @ href h) + ~input:(module (val data)) ~output:(module Data.Junit) set ; + signal + +(* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli new file mode 100644 index 0000000000000000000000000000000000000000..8bd97b3a34b424f98258308237381ca8d3971736 --- /dev/null +++ b/src/plugins/server/states.mli @@ -0,0 +1,42 @@ +(**************************************************************************) +(* *) +(* 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). *) +(* *) +(**************************************************************************) + +val register_value : + page:Doc.page -> + name:string -> + descr:Markdown.text -> + ?details:Markdown.block -> + output:'a Request.output -> + get:(unit -> 'a) -> + Request.signal + +val register_state : + page:Doc.page -> + name:string -> + descr:Markdown.text -> + ?details:Markdown.block -> + data:'a Data.data -> + get:(unit -> 'a) -> + set:('a -> unit) -> + Request.signal + +(* -------------------------------------------------------------------------- *)