fix: better error message on missing declaration name for docstring

When elaborating partial syntax, the elaborator sometimes attempts to
add a docstring for a declaration that it didn't parse a name for. The
name defaults to anonymous, but inserting the docs for the anonymous
name throws a panic about being on the wrong async branch.

With this change, the reported error is the expected parser error
instead, which is much friendlier.

Author: david-christiansen

src/Lean/DocString/Add.lean

@@ -206,10 +206,12 @@ Adds an elaborated Verso docstring to the environment.
 -/
 def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m]
     (declName : Name) (docs : VersoDocString) : m Unit := do
-  let throwImported {α} : m α :=
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  -- The decl name can be anonymous due to attempts to elaborate incomplete syntax. If the name is
+  -- anonymous, the `MapDeclarationExtension.insert` panics due to not being on the right async
+  -- branch. Better to just do nothing.
+  if declName.isAnonymous then return
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwImported
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
   modifyEnv fun env =>
     versoDocStringExt.insert env declName docs
 

tests/lean/versoDocMissing.lean

@@ -0,0 +1,9 @@
+set_option doc.verso true
+
+/-!
+This test checks that the error produced for a docstring without a corresponding declaration is a parser error instead of an internal error or panic from elaborating partial syntax.
+-/
+
+/--
+foo
+-/

tests/lean/versoDocMissing.lean.expected.out

@@ -0,0 +1 @@
+versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'