module Main:sig
..end
Server Main Process
typejson =
Json.t
typekind =
[ `EXEC | `GET | `SET ]
val string_of_kind : kind -> string
val pp_kind : Stdlib.Format.formatter -> kind -> unit
val register : kind -> string -> (json -> json) -> unit
val find : string -> (kind * (json -> json)) option
val exec : string -> json -> json
type
signal
val signal : string -> signal
val signal_name : signal -> string
type'a
request =[ `Kill of 'a
| `Poll
| `Request of 'a * string * json
| `Shutdown
| `SigOff of string
| `SigOn of string ]
Type of request messages. Parametrized by the type of request identifiers.
type'a
response =[ `CmdLineOff
| `CmdLineOn
| `Data of 'a * json
| `Error of 'a * string
| `Killed of 'a
| `Rejected of 'a
| `Signal of string ]
Type of response messages. Parametrized by the type of request identifiers.
type 'a
message = {
|
requests : |
|
callback : |
}
A paired request-response message. The callback will be called exactly once for each received message.
type 'a
server
val create : pretty:(Stdlib.Format.formatter -> 'a -> unit) ->
?equal:('a -> 'a -> bool) ->
fetch:(unit -> 'a message option) -> unit -> 'a server
Run a server with the provided low-level network primitives to actually
exchange data. Logs are monitored unless ~logs:false
is specified.
Default equality is the standard `(=)` one.
val start : 'a server -> unit
Start the server in background.
The function returns immediately after installing a daemon that (only)
accepts GET requests received by the server on calls to Db.yield()
.
Shall be scheduled at command line main stage via
Db.Main.extend
extension point.
val stop : 'a server -> unit
Stop the server if it is running in background.
Can be invoked to force server shutdown at any time.
It shall be typically scheduled via Extlib.safe_at_exit
along with
other system cleanup operations to make sure the server is property
shutdown before Frama-C main process exits.
val run : 'a server -> unit
Run the server forever.
The server would now accept any kind of requests and start handling them.
While executing an `EXEC
request, the server would
continue to handle (only) `GET
pending requests on Db.yield()
at every server.polling
time interval.
The function will not return until the server is actually shutdown.
Shall be scheduled at normal command line termination via
Cmdline.at_normal_exit
extension point.
val kill : unit -> 'a
Kill the currently running request by raising an exception.
val emit : signal -> unit
Emit the server signal to the client.
val on_signal : signal -> (bool -> unit) -> unit
Register a callback on signal listening.
The callback is invoked with true
on SIGON
command
and false
on SIGOFF
.
val on : (bool -> unit) -> unit
Register a callback to listen for server activity. All callbacks are executed in their order of registration. Callbacks shall never raise any exception.