feat: more metadata for Verso docstrings (#10560)

This PR adds highlighted Lean code to Verso docstrings and fixes smaller
quality-of-life issues.

Author: david-christiansen

src/Lean/Elab/DocString.lean

@@ -1171,23 +1171,21 @@ register_builtin_option doc.verso.suggestions : Bool := {
 -- during bootstrapping, the names in question may not yet be defined, so builtin
 -- names need special handling.
 private def suggestionName (name : Name) : TermElabM Name := do
-  try
-    if (← getEnv).contains name then
-      unresolveNameGlobalAvoidingLocals name
-    else
-      builtinFallback
-  catch
-    | _ => builtinFallback
-where
-  builtinFallback := do
-    let name' ←
-      if (← builtinDocRoles.get).contains name then pure (some name)
-      else if (← builtinDocCodeBlocks.get).contains name then pure (some name)
-      else pure none
-    match name' with
-      | some (.str _ s) => return .str .anonymous s
-      | some n => return n
-      | none => return name
+  let name' ←
+    -- Builtin expander names never need namespacing
+    if (← builtinDocRoles.get).contains name then pure (some name)
+    else if (← builtinDocCodeBlocks.get).contains name then pure (some name)
+    else pure none
+  match name' with
+    | some (.str _ s) => return .str .anonymous s
+    | some n => return n
+    | none =>
+      -- If it exists, unresolve it
+      if (← getEnv).contains name then
+        unresolveNameGlobalAvoidingLocals name
+      else
+        -- Fall back to doing nothing
+        pure name
 
 private def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggestion :=
   let cmp : (x y : Meta.Tactic.TryThis.SuggestionText) → Bool