Exotic error behaviour?

Stream: lean4

[Damiano Testa]

Dear All,

if you look at the code below, the error message under [new| f] informs me that elaboration function for '«term[new|_]»' has not been implemented [new|f] and then continues on to print all the comments below. Is this expected?

Thanks!

declare_syntax_cat new
syntax ident : new
syntax "[new|" new "]" : term

def my_error_prints_the_comments_below : new := [new| f]
-- The quick brown fox jumps over the lazy dog.
-- two lines
/-
The five boxing wizards jump quickly.
-/

/-
Lorem ipsum...
-/

/- still going on -/

-- the stream continues

--/-  This is printed. -/

/-  am I printed? -/

-- how can it stop?

[Arthur Paulino]

I confirm this on leanprover/lean4:nightly-2022-05-04
Which version are you using @Damiano Testa ?

[Damiano Testa]

If I understand correctly, I think that this is leanprover/lean4:nightly-2022-06-02 (this is the text that the file lean-toolchain contains.)

[Sebastian Ullrich]

It is a very least not a direct bug because that information is part of the concrete syntax tree of the term

[Damiano Testa]

I feel like this:
image.png