Command: EditAt - siegebell/vscoq GitHub Wiki

EditAt(stateId: integer)

Move focus to ${stateId}, such that commands may be added to the new state ID.

<call val="Edit_at"><state_id val="${stateId}"/></call>

Returns

Simple backtrack; focused stateId becomes the parent state

<value val="good">
  <union val="in_l"><unit/></union>
</value>

New focus; focusedQedStateId is the closing Qed of the new focus; senteneces between the two should be cleared

<value val="good">
  <union val="in_r">
    <pair>
      <state_id val="${focusedStateId}"/>
      <pair>
        <state_id val="${focusedQedStateId}"/>
        <state_id val="${oldFocusedStateId}"/>
      </pair>
    </pair>
  </union>
</value>

Failure: If stateId is in an error-state and cannot be jumped to, errorFreeStateId is the parent state of ``stateId` that shopuld be edited instead.

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

⚠️ GitHub.com Fallback ⚠️