WP Tactics

plugins.wp.tac.kind (DATA)

Parameter kind

kind ::= "checkbox" | "spinner" | "selector" | "browser" | "editor"

plugins.wp.tac.status (DATA)

Tactical status

status ::= "NotApplicable" | "NotConfigured" | "Applicable"

plugins.wp.tac.value (DATA)

Parameter option value

value ::= { "id" : $value , "label" : string , "title" : string }

plugins.wp.tac.parameter (DATA)

Parameter configuration

parameter ::= { fields… }

Field Format Description
"id" $param Parameter identifier
"kind" kind Parameter kind
"label" string Short name
"title" string Description
"enabled" boolean Enabled parameter
"value" any Value (with respect to kind)
"vmin" (opt.) number Minimum range value (spinner only)
"vmax" (opt.) number Maximum range value (spinner only)
"vstep" (opt.) number Range step (spinner only)
"vlist" (opt.) value [] List of options (selector only)

plugins.wp.tac.tactical (ARRAY)

Tactical Configurations

plugins.wp.tac.signalTactical (SIGNAL)

Signal for array tactical

plugins.wp.tac.tacticalData (DATA)

Data for array rows tactical

tacticalData ::= { fields… }

Field Format Description
"id" tactic Entry identifier.
"label" string Tactic name
"title" string Tactic description
"error" (opt.) string Tactic error
"status" status Tactic status
"params" parameter [] Configuration parameters

plugins.wp.tac.fetchTactical (GET)

Data fetcher for array tactical

input ::= number

output ::= { output… }

Output Format Description
"reload" boolean array fully reloaded
"removed" tactic [] removed entries
"updated" tacticalData [] updated entries
"pending" number remaining entries to be fetched

plugins.wp.tac.reloadTactical (GET)

Force full reload for array tactical

input ::= null

output ::= null

plugins.wp.tac.configureTactics (EXEC)

Configure all tactics

input ::= node

output ::= null

signals

plugins.wp.tac.setParameter (EXEC)

Configure tactical parameter

input ::= { input… }

output ::= null

Input Format Description
"node" node Proof node target
"tactic" tactic Tactic to configure
"param" $param Parameter to configure
"value" any New parameter value

plugins.wp.tac.applyTactic (EXEC)

Applies the (configured) tactic

input ::= tactic

output ::= node []

plugins.wp.tac.applyTacticAndProve (EXEC)

Applies tactic and run provers on children

input ::= tactic

output ::= node []