Syntax.prettyPrint has lots of space

Stream: lean4

[James Gallicchio]

mwe:

import Lean

unsafe def main : IO Unit := do
  let syn : Except _ Lean.Syntax ← Lean.withImportModules
    (imports := #[])
    (opts := default)
    (trustLevel := 0)
    <| fun env => EIO.toIO' <|
    Lean.Core.CoreM.run'
      (ctx := {
        fileName := "Example.lean"
        fileMap := default
      })
      (s := {
        env
      })
      (Lean.liftCommandElabM <| do
        `(def hi (x : Int) := sorry))
  match syn with
  | .error exc =>
    IO.println (← exc.toMessageData.toString)
  | .ok syn =>
  IO.println (syn.prettyPrint.pretty)

#eval main
-- def  hi  (  x  :  Int  )  :=  sorry

Is there some way I can prettyprint the syntax without so much extra whitespace?

[Eric Wieser]

There's a better function inside the PrettyPrinter namespace

[James Gallicchio]

aha, thanks!

updated MWE for my own future reference:

import Lean

unsafe def main : IO Unit := do
  let syn : Except _ Lean.Format ← Lean.withImportModules
    (imports := #[])
    (opts := default)
    (trustLevel := 0)
    <| fun env => EIO.toIO' <|
    Lean.Core.CoreM.run'
      (ctx := {
        fileName := "Example.lean"
        fileMap := default
      })
      (s := {
        env
      })
      (do
        let opt ← Lean.liftCommandElabM (do
          let int := Lean.mkIdent ``Unit
          `(opaque hi (x : $int) : $int))
        Lean.PrettyPrinter.formatCommand opt
      )
  match syn with
  | .error exc =>
    IO.println (← exc.toMessageData.toString)
  | .ok syn =>
  IO.println (syn.pretty)

#eval main --opaque hi.1 (x.1 : Unit) : Unit