Server.States
Synchronized values between Server and Client
val register_hook : Request.signal -> 'a callback -> unit
Connect a hook registry to a signal. As soon as the signal is being traced, a hook to emit the signal is registered.
val register_value :
package:Package.package ->
name:string ->
descr:Frama_c_kernel.Markdown.text ->
output:'a Request.output ->
get:( unit -> 'a ) ->
?add_hook:'b callback ->
unit ->
Request.signal
Register a (projectified) value and generates the associated signal and request:
<name>.sig
is emitted on value updates;<name>.get
returns the current value.If provided, the ~add_hook
option is used to register a hook to notify the server of value updates. The hook will be installed only once the client starts to listen for value updates.
Inside Ivette you can use the States.useSyncValue(id)
hook to synchronize with this value.
val register_state :
package:Package.package ->
name:string ->
descr:Frama_c_kernel.Markdown.text ->
data:'a Data.data ->
get:( unit -> 'a ) ->
set:( 'a -> unit ) ->
?add_hook:'b callback ->
unit ->
Request.signal
Register a (projectified) state and generates the associated signal and requests:
<name>.sig
is emitted on value updates;<name>.get
returns the current value;<name>.set
modifies the server value.If provided, the ~add_hook
option is used to register a hook to notify the server of value updates. The hook will be installed only once the client starts to listen for value updates.
Inside Ivette you can use the States.useSyncState(id)
hook to synchronize with this state.
val model : unit -> 'a model
Creates an empty array model.
val column :
name:string ->
descr:Frama_c_kernel.Markdown.text ->
data:'b Request.output ->
get:( 'a -> 'b ) ->
?default:'b ->
'a model ->
unit
Populate an array model with a new field. If a ~default
value is given, the field becomes optional and the field is omitted when equal to the default value (compared with =
).
val option :
name:string ->
descr:Frama_c_kernel.Markdown.text ->
data:'b Request.output ->
get:( 'a -> 'b option ) ->
'a model ->
unit
Populate an array model with a new optional field.
val reload : 'a array -> unit
Mark the array to be fully reloaded.
val update : 'a array -> 'a -> unit
Mark an array entry as updated.
val remove : 'a array -> 'a -> unit
Mark an array entry as removed.
val signal : 'a array -> Request.signal
Get the signal associated with the array.
val register_array :
package:Package.package ->
name:string ->
descr:Frama_c_kernel.Markdown.text ->
key:( 'a -> string ) ->
?keyName:string ->
?keyType:Package.jtype ->
iter:'a callback ->
?add_update_hook:'a callback ->
?add_remove_hook:'a callback ->
?add_reload_hook:unit callback ->
'a model ->
'a array
Register everything necessary to synchronize an array with the client:
<name>.sig
is emitted on array updates;<name>.fetch
is registered to get updates;<name>.reload
is registered to trigger a full reload.The ~key
parameter is used to identify array entries, and used to fill the reserved column "id"
of entries.
Columns added to the model after registration are not taken into account.
If provided, the ~add_xxx_hook
options are used to register hooks to notify the server of corresponding array updates. Each hook will be installed only once the client starts to listen for array updates.
Inside Ivette you can obtain the entries in sync by using the States.useSyncArray()
hook.