#guard_msgs command for testing commands

This module defines a command to test that another command produces the expected messages. See the docstring on the #guard_msgs command.

Element that can be part of a #guard_msgs specification.

Instances For

    Specification for #guard_msgs command.

    Instances For

      #guard_msgs captures the messages generated by another command and checks that they match the contents of the docstring attached to the #guard_msgs command.

      Basic example:

      error: unknown identifier 'x'
      #guard_msgs in
      example : α := x

      This checks that there is such an error and then consumes the message entirely.

      By default, the command intercepts all messages, but there is a way to specify which types of messages to consider. For example, we can select only warnings:

      warning: declaration uses 'sorry'
      #guard_msgs(warning) in
      example : α := sorry

      or only errors

      #guard_msgs(error) in
      example : α := sorry

      In this last example, since the message is not intercepted there is a warning on sorry. We can drop the warning completely with

      #guard_msgs(error, drop warning) in
      example : α := sorry

      Syntax description:

      #guard_msgs (drop? info|warning|error|all,*)? in cmd

      If there is no specification, #guard_msgs intercepts all messages. Otherwise, if there is one, the specification is considered in left-to-right order, and the first that applies chooses the outcome of the message:

      • info, warning, error: intercept a message with the given severity level.
      • all: intercept any message (so #guard_msgs in cmd and #guard_msgs (all) in cmd are equivalent).
      • drop info, drop warning, drop error: intercept a message with the given severity level and then drop it. These messages are not checked.
      • drop all: intercept a message and drop it.

      For example, #guard_msgs (error, drop all) in cmd means to check warnings and then drop everything else.

      Instances For

        The decision made by a specification for a message.

        Instances For

          Parses a guardMsgsSpec.

          • No specification: check everything.
          • With a specification: interpret the spec, and if nothing applies pass it through.
          Instances For
            • res : String

              The result of the nested command

            An info tree node corresponding to a failed #guard_msgs invocation, used for code action support.

            Instances For

              A code action which will update the doc comment on a #guard_msgs invocation.

              Instances For