pretty printing syntax quotations

Stream: lean4

[Damiano Testa]

I copy-pasted some command to obtain a pretty-printed format and I get an error in the example below: am I using this wrong?

import Lean.Elab.Command

open Lean Elab Command in
elab "pretty " cmd:command : command => do
  let fmt ← liftCoreM do PrettyPrinter.ppCategory `command cmd
  dbg_trace fmt

-- fails, the `|` in `command|` confuses `pretty`
pretty run_cmd `(command| end)
/-
unknown constant '«|»'
-/

-- works
pretty run_cmd `(end)
/-
run_cmd
  `(end)
-/

[Sebastian Ullrich]

#lean4 > prettyprint command quotation

[Damiano Testa]

Thanks! And I had even looked for some related topic before posting! :man_facepalming: