Discriminate doc comments from single line comments

[Luni-4]

It would be helpful to discriminate doc comments (///) from single line comments (//). Currently, they are assigned to the same token

[aryx]

Just curious, what is your use case? why do you need to discriminate them?

[bestouff]

I find it more ergonomic to see at a glance where doc comments are, and which parts of code have (or have no) doc comments.

[Luni-4]

Just curious, what is your use case? why do you need to discriminate them?

It would be helpful to compute metrics that determine how much a code is documented in percentage

[locnide]

Just curious, what is your use case? why do you need to discriminate them?

Another usecase mentioned in #99 (comment) is to highlight doc comments as they are markdown. It would be especially useful for long documentation, like in modules.

[maddiemort]

Should this be reopened? It looks like the changes from #99 were immediately reverted.