downstream: update repo verso

downstream-repo: verso
downstream-url: https://github.com/leanprover/verso
downstream-rev: main
downstream-sha: 5f675d7d20aa9391a7fea01429601f94e850e159

Author: downstream-lean4[bot]

verso/src/tests/Tests/LiterateHtml.lean

@@ -224,6 +224,9 @@ private def testAllBuiltinDocRoles (data : TestData) : IO Unit := withTestDir da
   unless hasSubstring jsonContent "\"content\":\"lhs\",\"kind\":{\"keyword\":{\"docs\":\"" do
     throw <| IO.userError "Builtins JSON has no docs on the `lhs` keyword token. \
       The conv handler did not attach the syntax kind's docstring."
+  unless hasSubstring jsonContent "{\"content\":\"funext\",\"kind\":{\"keyword\":{\"docs\":\"" do
+    throw <| IO.userError "Builtins JSON has no docs on the `funext` keyword token. \
+      The kw handler did not attach the syntax kind's docstring."
 
 /--
 Checks that user-registered `@[inline_to_literate]` and `@[block_to_literate]` handlers shadow the

verso/src/verso-literate/VersoLiterate/Basic.lean

@@ -173,12 +173,13 @@ def handleConvTactic : InlineToLiterate
   | _, _, _ => pure none
 
 def handleKwAtom : InlineToLiterate
-  | name, _val, content => do
-    -- Data.Atom is mistakenly marked private in Lean. Here's a workaround until we fix that.
-    -- Check the name's suffix because private names have a mangled prefix:
-    unless name.toString.endsWith "Lean.Doc.Data.Atom" do return none
-    let some s := (match content with | #[.code s] => some s | _ => none) | return none
-    return some <| .other (.highlighted <| .token ⟨.keyword none none none, s⟩) content
+  | ``Lean.Doc.Data.Atom, val, content => do
+    if let some { name, .. } := val.get? Lean.Doc.Data.Atom then
+      let #[.code s] := content | return none
+      let docs ← findDocString? (← getEnv) name
+      return some <| .other (.highlighted <| .token ⟨.keyword (some name) none docs, s⟩) content
+    throwError "Wrong data"
+  | _, _, _ => pure none
 
 def handleSyntax : InlineToLiterate
   | ``Lean.Doc.Data.Syntax, val, content => do

verso/test-projects/literate-config/LitConfig/Builtins.lean

@@ -31,7 +31,7 @@ set_option doc.verso.suggestions false in
 
 {syntaxCat}`term` is a syntax category, and {syntax term}`1 + [] - (· / ·)` is syntax in it.
 
-{kw (of := Lean.«command__Unif_hint____Where_|_-⊢__»)}`unif_hint` is a keyword atom.
+{kw}`funext` is a keyword atom.
 {kw? (of := Lean.«command__Unif_hint____Where_|_-⊢__»)}`where` is also a keyword atom, and
 {kw! (of := Lean.Parser.Command.definition)}`def` is an unchecked keyword atom.