module doc comments

Stream: lean4

[Mario Carneiro]

This definition of module doc comments doesn't work, because the lexer has a special case for /-- comments that does not extend to /-!. As a result, module doc comments don't show up in the parse tree and can't be reparsed even with a command parser like this:

@[commandParser] def modDocComment := leading_parser ppDedent $ "/-!" >> commentBody >> ppLine