syntax with linebreaks

Stream: metaprogramming / tactics

[Ajay Kumar Nair]

syntax yamlEnt := yamlIdent ":" lineEq str
syntax yamlEnts:= many(yamlEnt linebreak)

syntax "yamlEntries" yamlEnts  : term

| `(yamlEntries $[$names:yamlIdent: $values:str]*) => do
  let names: Array (TSyntax `term) ← names.mapM fun
    | `(yamlIdent| $name: ident) => pure (name.getId |> toString |> quote)
    | `(yamlIdent| $name: str) => pure name
    | _ => Macro.throwUnsupported
  `(Lean.Json.mkObj [$[($names, $values)],*])

This gives me the following error message :

unexpected token '$'; expected ')'

I am unable to spot the error. What is the syntax for matching syntax with linebreaks?

[Robin Arnez]

You said linebreak, so you gotta linebreak:

syntax yamlIdent := ident <|> str
syntax yamlEnt := yamlIdent ":" lineEq str
syntax yamlEnts:= many(yamlEnt linebreak)

syntax "yamlEntries" yamlEnts  : term

open Lean

macro_rules
| `(yamlEntries $[$names:yamlIdent: $values:str
]*) => do
  let names: Array (TSyntax `term) ← names.mapM fun
    | `(yamlIdent| $name: ident) => pure (name.getId |> toString |> quote)
    | `(yamlIdent| $name: str) => pure name
    | _ => Macro.throwUnsupported
  `(Lean.Json.mkObj [$[($names, $values)],*])