Lean4
@[inherit_doc Mathlib.Linter.linter.ppRoundtrip]
def ppRoundtrip : Linter where
run :=
withSetOptionIn fun stx ↦ do
unless getLinterValue linter.ppRoundtrip (← getLinterOptions) do
return
if (← MonadState.get).messages.hasErrors then
return
let stx := capSyntax stx (stx.getTailPos?.getD default).1
let origSubstring := stx.getSubstring?.getD default
let (real, lths) := polishSource origSubstring.toString
let fmt ←
(liftCoreM do
PrettyPrinter.ppCategory `command stx <|>
(do
Linter.logLint linter.ppRoundtrip stx
m!"The ppRoundtrip linter had some parsing issues: \
feel free to silence it with `set_option linter.ppRoundtrip false in` \
and report this error!"
return real))
let st := polishPP fmt.pretty
if st != real then
let diff := real.firstDiffPos st
let pos := posToShiftedPos lths diff.1 + origSubstring.startPos.1
let f := origSubstring.str.drop (pos)
let extraLth := (f.takeWhile (· != st.get diff)).length
let srcCtxt := zoomString real diff.1 5
let ppCtxt := zoomString st diff.1 5
Linter.logLint linter.ppRoundtrip (.ofRange ⟨⟨pos⟩, ⟨pos + extraLth + 1⟩⟩)
m! "source context\n'{srcCtxt }'\n'{ppCtxt}'\npretty-printed context"
