diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 2ca3496630..e9e884aa44 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -16,7 +16,7 @@ def commentBody : Parser := @[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken @[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -def docComment := leading_parser ppDedent $ "/--" >> commentBody >> ppLine +def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine end Command builtin_initialize