Extended /-" strings "-/

Stream: lean4

[Eric Wieser]

In Lean3, we had an extended string notation that allowed things like

#eval /-"<a href="#">The quotes in here are fine</a>"-/

which not only allows unescaped quotes within the /- -/, but also gives html syntax highlighting.
This is a bit like pythons """ triple "quoted" strings"""

Does Lean4 have any analogous string literals? Or do I have no choice but to escape all my inner "s?

[Patrick Massot]

See previous discussion starting at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Macro.20for.20testing.20error.20messages/near/278412091

[Eric Wieser]

Thanks!

[Patrick Massot]

And I would also love to see this in Lean 4.

[James Gallicchio]

most important message from linked discussion:
Sebastian Ullrich said:

I created a separate issue at least: https://github.com/leanprover/lean4/issues/1422
Feel free to upvote important issues I'd say, we could use that for prioritization

it's already the most upvoted feature that isn't mathlib high priority, but more thumbs is always good :P

[Patrick Massot]

Indeed I forgot about this issue but I upvoted at that time.