Newline-sensitive syntax

Stream: lean4

[Marcus Rossel]

How can I create a syntax that uses newlines to differentiate between syntax objects?
For example, if I have:

declare_syntax_cat map_field
declare_syntax_cat map_row

syntax "•" : map_field
syntax "▦" : map_field

syntax map_field+ "\n" : map_row
syntax:max map_row+ : term

... Lean complains with invalid parser 'map_row_', invalid empty symbol.
If I add an explicit terminating symbol (syntax map_field+ "|\n" : map_row ), it works.
But is there a way to avoid the terminating symbol?

[Alex Keizer]

Try linebreak instead of "\n"

declare_syntax_cat map_field
declare_syntax_cat map_row

syntax "•" : map_field
syntax "▦" : map_field

syntax map_field+ linebreak : map_row
syntax:max map_row+ : term

[Marcus Rossel]

Alex Keizer said:

Try linebreak instead of "\n"

syntax map_field+ linebreak : map_row
syntax:max map_row+ : term

Cool, that fixes the error - thanks!
Now I'm having problems defining the associated macro rule though. For example, in the following:

def x :=
  ••••
  ▦▦▦▦
  ••▦▦

macro_rules
  | `($rows:map_row*) => do
    for row in rows do
      dbg_trace s!"{row}" -- this is only called once

... the rows list only has a single element instead of three. How can I distinguish between the lines here?

[Alex Keizer]

Right, map_field+ use whitespace as a delimiter, and newlines count as whitespace, so it goes by the longest match
I guess you want a many1 syntax which doesn't accept newlines as delimiters. Not sure how to do that, though

[Sebastian Ullrich]

Untested: map_field (noWs map_field)* linebreak

[Marcus Rossel]

Sebastian Ullrich said:

Untested: map_field (noWs map_field)* linebreak

Like this?

syntax map_field (noWs map_field)* linebreak : map_row
syntax:max map_row+ : term

Because that still produces just a single row in

macro_rules
  | `($rows:map_row*) =>

[Alex Keizer]

Really? For me the following code parses x into three separate rows

declare_syntax_cat map_field
declare_syntax_cat map_row

syntax "•" : map_field
syntax "▦" : map_field

syntax map_field (noWs map_field)* linebreak : map_row
syntax:max map_row+ : term


macro_rules
  | `($rows:map_row*) => do
    dbg_trace "rows: {rows.size}"
    for row in rows do
      dbg_trace s!"{row}" --
    `(1)

def x :=
  ••••
  ▦▦▦▦
  ••▦▦