Lean4
/-- Formatter for the script parser. -/
def formatter (name : String) (m : Mapping) (k : SyntaxNodeKind) (p : Formatter) : Formatter := do
let stack ← modifyGet fun s => (s.stack, { s with stack := #[] })
Formatter.node.formatter k p
let st ← get
let transformed : Except String _ :=
st.stack.mapM
(·.mapStringsM fun s => do
let some s := s.toList.mapM (m.toSpecial.insert ' ' ' ').get? |
.error s
.ok ⟨s⟩)
match transformed with
| .error err =>
-- TODO: this only appears if the caller explicitly calls the pretty-printer
Lean.logErrorAt (← get).stxTrav.cur s! "Not a {name }: '{err}'"
set { st with stack := stack ++ st.stack }
| .ok newStack =>
set { st with stack := stack ++ newStack }