#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.

opaque guard_msgs.diff : Lean.Option Bool

inductive Lean.Elab.Tactic.GuardMsgs.SpecResult : Type

The decision made by a specification for a message.

• check : SpecResult

  Capture the message and check it matches the docstring.

• drop : SpecResult

  Drop the message and delete it.

• pass : SpecResult

  Do not capture the message.

inductive Lean.Elab.Tactic.GuardMsgs.WhitespaceMode : Type

The method to use when normalizing whitespace, after trimming.

• exact : WhitespaceMode

  Exact equality.

• normalized : WhitespaceMode

  Equality after normalizing newlines into spaces.

• lax : WhitespaceMode

  Equality after collapsing whitespace into single spaces.

inductive Lean.Elab.Tactic.GuardMsgs.MessageOrdering : Type

Method to use when combining multiple messages.

• exact : MessageOrdering

  Use the exact ordering of the produced messages.

• sorted : MessageOrdering

  Sort the produced messages.

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsFilterAction (action? : Option (TSyntax `Lean.guardMsgsFilterAction)) : Command.CommandElabM SpecResult

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsFilterSeverity : TSyntax `Lean.guardMsgsFilterSeverity → Command.CommandElabM (Message → Bool)

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsSpec (spec? : Option (TSyntax `Lean.guardMsgsSpec)) : Command.CommandElabM (WhitespaceMode × MessageOrdering × (Message → SpecResult))

Parses a guardMsgsSpec.

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

structure Lean.Elab.Tactic.GuardMsgs.GuardMsgFailure : Type

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

• res : String

  The result of the nested command

instance Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure : TypeName GuardMsgFailure

def Lean.Elab.Tactic.GuardMsgs.revealTrailingWhitespace (s : String) : String

Makes trailing whitespace visible and protectes them against trimming by the editor, by appending the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid ambiguities in the case the message already had that symbol).

def Lean.Elab.Tactic.GuardMsgs.removeTrailingWhitespaceMarker (s : String) : String

def Lean.Elab.Tactic.GuardMsgs.WhitespaceMode.apply (mode : WhitespaceMode) (s : String) : String

Applies a whitespace normalization mode.

def Lean.Elab.Tactic.GuardMsgs.MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List String

Applies a message ordering mode.

def Lean.Elab.Tactic.GuardMsgs.elabGuardMsgs : Command.CommandElab

def Lean.Elab.Tactic.GuardMsgs.guardMsgsCodeAction : CodeAction.CommandCodeAction

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