From f1bb524360ef014393fd505f143ab6cc54dde719 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 12 Aug 2024 11:01:44 -0700 Subject: [PATCH] touch up wording, add comment --- src/Lean/Elab/BuiltinCommand.lean | 3 ++- tests/lean/interactive/3135.lean.expected.out | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index da4cf746d475..79987295c66a 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -24,10 +24,11 @@ namespace Lean.Elab.Command | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}" @[builtin_command_elab looseDocComment] def elabLooseDocComment : CommandElab := fun stx => do + -- def looseDocComment := leading_parser ppDedent (docComment >> optional commandParser) let trailingKind := stx[1][0].getKind let addlHint := if trailingKind == ``Lean.Parser.Command.in then - "\n\nHint: the docstring must come after '... in', immediately before the declaration that accepts a docstring." + "\n\nHint: the docstring must come after the 'in' keyword, immediately before the declaration that accepts a docstring." else "" logError m!"unexpected doc string{addlHint}" diff --git a/tests/lean/interactive/3135.lean.expected.out b/tests/lean/interactive/3135.lean.expected.out index 41f80797e1bd..9a712377e584 100644 --- a/tests/lean/interactive/3135.lean.expected.out +++ b/tests/lean/interactive/3135.lean.expected.out @@ -13,7 +13,7 @@ "range": {"start": {"line": 14, "character": 0}, "end": {"line": 15, "character": 0}}, "message": - "unexpected doc string\n\nHint: the docstring must come after '... in', immediately before the declaration that accepts a docstring.", + "unexpected doc string\n\nHint: the docstring must come after the 'in' keyword, immediately before the declaration that accepts a docstring.", "fullRange": {"start": {"line": 14, "character": 0}, "end": {"line": 17, "character": 10}}},