feat: make loose docstrings into elaboration errors rather than parse errors

src/Lean/Elab/BuiltinCommand.lean

@@ -23,6 +23,18 @@ namespace Lean.Elab.Command
      modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
    | _ => 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 the 'in' keyword, immediately before the declaration that accepts a docstring."
+    else
+      ""
+  logError m!"unexpected doc string{addlHint}"
+  if stx[1].getNumArgs == 1 then
+    elabCommand stx[1]
+
 private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
     env    := s.env.registerNamespace newNamespace,

src/Lean/Parser/Command.lean

@@ -53,6 +53,13 @@ multiple times in the same file.
 def moduleDoc := leading_parser ppDedent <|
   "/-!" >> commentBody >> ppLine
 
+-- A low-priority parser to be able to log an error that it's not attached to anything.
+-- This is more friendly than a parser error, and it saves needing to add `docComment` before
+-- every command that doesn't accept a doc comment.
+-- It is trailed by an optional command so that the error can give a hint.
+@[builtin_command_parser low]
+def looseDocComment := leading_parser ppDedent (docComment >> optional commandParser)
+
 def namedPrio := leading_parser
   atomic (" (" >> nonReservedSymbol "priority") >> " := " >> withoutPosition priorityParser >> ")"
 def optNamedPrio := optional namedPrio

tests/lean/interactive/3135.lean

@@ -0,0 +1,29 @@
+/-!
+# Loose docstrings
+-/
+
+/-!
+Basic test
+-/
+
+section
+/-- This is a loose docstring -/
+--^ collectDiagnostics
+end
+
+section
+/-- This is a loose docstring before an 'in' command. -/
+--^ collectDiagnostics
+set_option pp.all true in
+def x := 0
+
+-- Still elaborates the `def`
+#check x
+     --^ textDocument/hover
+end
+
+section
+set_option pp.all true in
+/-- This is a docstring in its correct position. -/
+def y := 0
+end

tests/lean/interactive/3135.lean.expected.out

@@ -0,0 +1,32 @@
+{"version": 1,
+ "uri": "file:///3135.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 9, "character": 0}, "end": {"line": 10, "character": 0}},
+   "message": "unexpected doc string",
+   "fullRange":
+   {"start": {"line": 9, "character": 0}, "end": {"line": 11, "character": 3}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 14, "character": 0}, "end": {"line": 15, "character": 0}},
+   "message":
+   "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}}},
+  {"source": "Lean 4",
+   "severity": 3,
+   "range":
+   {"start": {"line": 20, "character": 0}, "end": {"line": 20, "character": 6}},
+   "message": "x : Nat",
+   "fullRange":
+   {"start": {"line": 20, "character": 0},
+    "end": {"line": 20, "character": 6}}}]}
+{"textDocument": {"uri": "file:///3135.lean"},
+ "position": {"line": 20, "character": 7}}
+{"range":
+ {"start": {"line": 20, "character": 7}, "end": {"line": 20, "character": 8}},
+ "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}