Feedback: Message - siegebell/vscoq GitHub Wiki

Communicates an unstructured (i.e. plaintext) message. level is one of {info,warning,notice,error,debug}. For example: in response to an Add(_,"Axiom foo: nat.",true), message foo is assumed will be emitted.

8.6

<feedback object="state" route="0">
  <state_id val="${stateId}"/>
  <feedback_content val="message">
    <message>
      <message_level val="${level}"/>
      <option val="some"><loc start="${start: int}" stop="${stop: int}"/></option>
      <richpp>${message}</richpp>
    </message>
  </feedback_content>
</feedback>

8.5

<feedback object="state" route="0">
  <state_id val="${stateId}"/>
  <feedback_content val="message">
    <message>
      <message_level val="${level}"/>
      <string>${message}</string>
    </message>
  </feedback_content>
</feedback>
Add a custom footer
⚠️ **GitHub.com Fallback** ⚠️