Command: Add - siegebell/vscoq GitHub Wiki

Adds a toplevel command (e.g. vernacular, definition, tactic) to the given state. verbose controls whether out-of-band messages will be generated for the added command (e.g. "foo is assumed" in response to adding "Axiom foo: nat.").

<call val="Add">
  <pair>
    <pair>
      <string>${command}</string>
      <int>${editId}</int>
    </pair>
    <pair>
      <state_id val="${stateId}"/>
      <bool val="${verbose}"/>
    </pair>
  </pair>
</call>

• The added command is given a fresh stateId and becomes the next "tip".

<value val="good">
  <pair>
    <state_id val="${newStateId}"/>
    <pair>
      <union val="in_l"><unit/></union>
      <string>${message}</string>
    </pair>
  </pair>
</value>

• When closing a focused proof (in the middle of a bunch of interpreted commands), the Qed will be assigned a prior stateId and nextStateId will be the id of an already-interpreted state that should become the next tip.

<value val="good">
  <pair>
    <state_id val="${stateId}"/>
    <pair>
      <union val="in_r"><state_id val="${nextStateId}"/></union>
      <string>${message}</string>
    </pair>
  </pair>
</value>

• Failure:
  • Syntax error. Error offsets are with respect to the start of the sentence.

  <value val="fail"
      loc_s="${startOffsetOfError}"
      loc_e="${endOffsetOfError}">
    <state_id val="${stateId}"/>
    ${errorMessage}
  </value>

  • Another error (e.g. Qed before goal complete)

  <value val="fail"><state_id val="${stateId}"/>${errorMessage}</value>