ppCommand on multiple commands

Stream: lean4

[James Gallicchio]

mwe

import Lean

open Lean Elab Command

syntax (name := generate_capnproto)
  "#generate_capnproto " term (" {{ " command* " }}" )? : command

@[command_elab generate_capnproto]
def genCapnProtoHandler : CommandElab := fun stx => do
  logInfo (
    ← liftCoreM <| Lean.PrettyPrinter.ppCommand (.mk stx)
  )

#generate_capnproto "hi" {{
  def what := 1
  def who := 2
}}
-- Prints out:
-- #generate_capnproto "hi" {{
--   def what :=
--     1def who :=
--     2 }}

Is there an easy way to get nicer output here?

[James Gallicchio]

the newline is missing no matter what commands you put in there and regardless of the line length; I got this output in my actual code before making the MWE:

  #check 5#check 6def «schema.capnp:Test» : Type :=
    CapnProtoLean.Struct instance : CapnProtoLean.Struct.IsStruct «schema.capnp:Test»
      where
    fromStruct := id
    expectedDataWords := 1
    expectedPtrWords := 2def «schema.capnp:Test».foo (self : «schema.capnp:Test») : UInt64 :=
    sorry def «schema.capnp:Test».bar (self : «schema.capnp:Test») : CapnProtoLean.List.P UInt64 :=
    sorry def «schema.capnp:Test».zing (self : «schema.capnp:Test») : CapnProtoLean.List.P «schema.capnp:Test» :=
    sorry

[Kyle Miller]

Here's a solution:

syntax (name := generate_capnproto)
  "#generate_capnproto " term (" {{ " ppDedent((ppLine command)* ppLine) " }}" )? : command

[Kyle Miller]

#generate_capnproto "hi" {{
def what :=
  1
def who :=
  2
 }}

[Kyle Miller]

Oh, I didn't need the ppDedent

[Kyle Miller]

Here:

syntax (name := generate_capnproto)
  "#generate_capnproto " term (" {{ " (ppLine command)* ppDedent(ppLine "}}") )? : command

yields

#generate_capnproto "hi" {{
  def what :=
    1
  def who :=
    2
}}

[James Gallicchio]

new parser combinator discovered :tada: