-- Init.Notation
/-- `/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.

Basic example:
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.

By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```

In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is
`(check all, whitespace := normalized, ordering := exact, positions := false)`.

Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.

The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.

Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
  (the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.

Message ordering:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
  This helps with testing commands that are non-deterministic in their ordering.

Position reporting:
- `positions := true` reports the ranges of all messages relative to the line on which
  `#guard_msgs` appears.
- `positions := false` does not report position info.

Substring matching:
- `substring := true` checks that the docstring appears as a substring of the output
  (after whitespace normalization). This is useful when you only care about part of the message.
- `substring := false` (the default) requires exact matching (modulo whitespace normalization).

Stabilizing output:
When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may
differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace
anonymous metavariables with `?_` while preserving user-named metavariables like `?a`.
Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`.
Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like
`_fvar.22` with `_fvar._`.

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

The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
 -/
Lean.guardMsgsCmd : Lean.ParserDescr