Syntax formatting

Stream: lean4

[Marx]

Hey y'all,

Is there any way to format syntax beyond just using newlines?

For example, in this mwe:

import Lean
open Lean Lean.Parser
open Lean PrettyPrinter Delaborator

declare_syntax_cat testSyntax

syntax "start" withPosition(semicolonOrLinebreak ppDedent(ppLine))
  num withPosition(semicolonOrLinebreak ppDedent(ppLine))
  num withPosition(semicolonOrLinebreak ppDedent(ppLine))
  "end": testSyntax

structure Test where
  test1: Nat
  test2: Nat

def numToIdent (t:TSyntax `term) : TSyntax `num := Unhygienic.run do
  match t with
  | `($n:num) => return n
  | _ => return ← `(num | 0)

@[app_unexpander Test.mk]
def TestUnexpander : Unexpander
  | `(Test.mk $n1 $n2) => do
    let id1 := numToIdent n1
    let id2 := numToIdent n2
    `(testSyntax | start
        $id1
        $id2
    end)
  | _ => throw Unit.unit

I want the numbers to be indented like this:

start
      1
      2
end

[Marx]

In case someone has the same question, here is my solution:

Its possible to format syntax with

ppDedent()
ppIndent()

Those are no-op parser combinators which take either another parser combinator or a no-op parser like this

ppSpace
ppLine

as argument. This lets you format the syntax with indents or newlines.