Syntax-aware document editing

Stream: lean4

[Edward Ayers]

Is there any plans or work underway to create a syntax-safe document editing component for the Lean server?

[Jakob von Raumer]

/cc @Sebastian Ullrich

[Sebastian Ullrich]

I assume you mean something better than manipulating the syntax tree, manually inserting whitespace as appropriate. One rough plan has always been to make the pretty printer good enough that you can just edit the structure of the syntax tree and then reformat the entire surrounding command.

[Sebastian Ullrich]

Or maybe I misunderstood you completely. Do you mean editing by the server or by a human user?

[Jakob von Raumer]

We were talking about the "code actions"

[Sebastian Ullrich]

That's what I hoped :)

[Edward Ayers]

What's the method to pretty print Syntax?

[Sebastian Ullrich]

It's ppCommand, see e.g. https://github.com/leanprover/lean4/blob/ef9976ccdaa7c19fe1208cf64b1f43b3c0811d1b/script/reformat.lean#L32