pretty printed string

Stream: lean4

[Damiano Testa]

Is there a way to get the output of pretty printed syntax as a string?

For example:

import Lean.Elab.Command

open Lean

run_cmd
  let stx ← `(variable {$(mkIdent `a) : $(mkIdent `X)})
  logInfo stx
-- variable {a : X}

How can I get the string "variable {a : X}" out of stx?

[Jannis Limperg]

import Lean.Elab.Command

open Lean PrettyPrinter Elab.Command

run_cmd do
  let stx ← `(variable {$(mkIdent `a) : $(mkIdent `X)})
  logInfo $ ← liftTermElabM $ ppCommand stx

For other syntax categories, see ppCategory etc.

[Jannis Limperg]

Then docs#Std.Format.pretty to convert Format to String.

[Damiano Testa]

Ah, Std.Format.pretty looks like it is exactly what I was missing! Thanks a lot!