elab not implemented picks up comments

Stream: lean4

[Mario Carneiro]

syntax "foo" : term
#eval foo
-- bla
-- baz

prints

elaboration function for 'termFoo' has not been implemented
  foo
    -- bla
    -- baz

note the presence of the comments in the error message

[Mario Carneiro]

This is I guess borderline on whether this is desired behavior

[Daniel Selsam]

FWIW it looks weird to me. My -- comments generally precede terms rather than follow them.

[Sebastian Ullrich]

Yes, there is a separate pass from parsing that associates whitespace/comments to the "correct" token. https://github.com/leanprover/lean4/blob/5fc1a86274369d69171f6db5096e98bb43d0a78a/src/Lean/Syntax.lean#L139-L154
We don't currently run it before elaboration, but I also think this error message is one of the few/the only one that actually prints out input syntax

[Sebastian Ullrich]

I think there are much bigger issues with this error message and how to debug it (when complex syntax pattern matches are involved) than showing unexpected comments. I'm not even sure if it shouldn't just show the raw syntax tree by default. Definitely not something a user not implementing their own syntax should ever see.