touch up wording, add comment

leanprover · Aug 12, 2024 · f1bb524 · f1bb524
1 parent dd77298
commit f1bb524
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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}}},