create newlines in Syntax

Stream: lean4

[Siddharth Bhat]

given an array of strings, how do I create a Lean.Syntax object that "vertically concatenates" these? here's what I've tried:

partial def stx_vgroup_strings (ss: Array String)
: Lean.PrettyPrinter.UnexpandM Lean.Syntax := do
  let mut out <- `("") -- how to get empty Lean.Syntax object?
  let newline <- `("\n") -- how to get newline?
  for s in ss do
    out :=  (<- `($out
                   $newline
                   $(Lean.quote s)))
  return out

Clearly, let newline <- ... is broken, since it creates the _string_ "\n", and not the "concept of newline in the syntax". What should I replace let newline <- ... by to create newlines?

[Sebastian Ullrich]

Currently syntax quotations always generate SourceInfo.syntheticwithout whitespace information; if you want to programmatically generate Syntax with SourceInfo.original, you need to do so yourself. Or invent a new kind of quotation :) .

[Siddharth Bhat]

Thanks, I'll try and forge a SourceInfo.original programatically :) When you say "invent a new kind of quotation", do you mean adding a new syntax like:

`<<
  whitespace sensitive quoter
   >>

which quotes in a whitespace sensitive fashion?

[Sebastian Ullrich]

Yes, though I think there are many unclear parts e.g. as to newlines and indentation. Which is part of why we didn't do it so far.

[Sebastian Ullrich]

The simplest solution when generating code would be to make the pretty printer good enough that quotations don't have to worry about formatting at all