Pretty printing comments

Stream: lean4

[Damiano Testa]

Given how well my previous pretty comment went, let me try again, this time with pretty-printing comments.

Should this also be modified?

import Lean.Elab.Command

open Lean Elab.Command in
elab "#pretty_print " cmd:command : command => do
  elabCommand cmd -- it is too weird if you do not elaborate the command!
  logInfo cmd

/--
info: variable (a : Nat) in
-- here is a simple exampleexample : a = a :=
  rfl
-/
#guard_msgs in
#pretty_print
variable (a : Nat) in
-- here is a simple example
example : a = a := rfl

[Jannis Limperg]

This is a long-standing issue: lean4#3791

[Damiano Testa]

Ah, yes, thanks for the link!

[Damiano Testa]

I had already upvoted it. I wish I could upvote it again, given that I had forgotten about it...

[Damiano Testa]

In case anyone wonders about where these pretty comment come from, it is thanks to the linter at #24465: it exploits the pretty printer as a source of how to format code, and has picked up a few pretty printing issues.

[Damiano Testa]

Come to think of it, Jannis, any chance that this looks reasonable to you? leanprover-community/aesop#203