Lean code fences that use +error in doc.verso docstrings make for broken :literateHtml output

[robsimmons]

To replicate, run the following in an empty directory:

echo "leanprover/lean4:v4.30.0-rc2" > lean-toolchain

cat > lakefile.toml <<EOL
name = "demo"
version = "0.1.0"
defaultTargets = ["Demo"]

[[lean_lib]]
name = "Demo"

[[require]]
name = "verso"
scope = "leanprover"
rev = "v4.30.0-rc2"
EOL

cat > Demo.lean <<EOL
set_option doc.verso true
/-!
\`\`\`lean +error
bogus nonsense
\`\`\`
-/
EOL

lake build :literateHtml

Expected: a valid literate HTML page is generated

Observed:

info: stderr:
error finding highlighted code: unexpected internal error: No block handler for Lean.Doc.Data.LeanBlock with type Lean.Doc.Data.LeanBlock
error: external command '/Users/rob/o/tmp/.lake/packages/verso/.lake/build/bin/verso-literate' exited with code 2
Some required targets logged failures:
- demo/Demo:literate
error: build failed