From ac73c8d342eeea466d2e1dfa8b3b62243bf9b6f4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 9 Nov 2023 23:00:34 +1100 Subject: [PATCH] feat: Lean.Linter.logLintIf (#2852) A utility function moving from Mathlib. --- src/Lean/Linter/Util.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index 5d5fa88701..62e487bbd4 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -10,6 +10,12 @@ def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := logWarningAt stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]") +/-- If `linterOption` is true, print a linter warning message at the position determined by `stx`. +-/ +def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] + (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do + if linterOption.get (← getOptions) then logLint linterOption stx msg + /-- Go upwards through the given `tree` starting from the smallest node that contains the given `range` and collect all `MacroExpansionInfo`s on the way up. The result is `some []` if no `MacroExpansionInfo` was found on the way and