formatter — Mathlib

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 }
Похожие утверждения