nested comment blocks

Stream: general

[Rob Lewis]

Cross-posting from #1963: Lean doesn't like nested comment blocks. e.g.

/-
/- -/
a
-/

ends the comment on the second line, and a is not commented. @Gabriel Ebner guessed it wouldn't be horribly hard to allow this. Does anyone agree/disagree with that guess, and is anyone interested in trying to implement it?

[Gabriel Ebner]

NB: it already works for regular comments. That is, Rob's example works as expected. It's docstrings that we want to nest. So if anybody wants to implement this, you can just copy the logic from the read_comment_block function!

[Rob Lewis]

Oh! I didn't even try it for the example I posted, I just assumed it would be the same.

[Rob Lewis]

Silly me for making assumptions.

[Bryan Gin-ge Chen]

Oops, I missed this discussion and just said roughly the same thing in the issue comments.

[Bryan Gin-ge Chen]

I gave this a shot: https://github.com/leanprover-community/lean/pull/113