fix: improve error name rendering in narrower viewports

This commit drops error name prefixes from the table and sidebar and allows hyphenation at reasonable split points.

Author: jrr6

Manual/ErrorExplanations.lean

@@ -38,6 +38,20 @@ inline_extension Inline.errorExplanationLink (errorName : Name) where
       logError s!"Could not find external tag for error explanation '{name}' corresponding to ID '{id}'"
       content.mapM go
 
+/- Renders the suffix of an error explanation, allowing line breaks before capital letters. -/
+inline_extension Inline.errorExplanationShortName (errorName : Name) where
+  data := toJson (getBreakableSuffix errorName)
+  traverse := fun _ _ _ => pure none
+  extraCss := [".error-explanation-short-name { hyphenate-character: ''; }"]
+  toTeX := none
+  toHtml := some fun _go _id info _content =>
+    open Verso.Output Html in do
+    let .ok (some errorName) := fromJson? (α := Option String) info
+      | HtmlT.logError "Invalid data for explanation name element"
+        pure .empty
+    let html := {{ <code class="error-explanation-short-name">{{errorName}}</code> }}
+    return html
+
 @[block_role_expander error_explanation_table]
 def error_explanation_table : BlockRoleExpander
   | #[], #[] => do
@@ -49,11 +63,10 @@ def error_explanation_table : BlockRoleExpander
     let headers ← #["Name", "Summary", "Severity", "Since"]
       |>.mapM fun s => ``(Verso.Doc.Block.para #[Doc.Inline.text $(quote s)])
     let vals ← entries.flatMapM fun (name, explan) => do
-      let sev := quote <|
-        if explan.metadata.severity == .warning then "Warning" else "Error"
+      let sev := quote <| if explan.metadata.severity == .warning then "Warning" else "Error"
       let sev ← ``(Doc.Inline.text $sev)
-      let nameStr := toString name
-      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name)) #[Doc.Inline.code $(quote nameStr)])
+      let nameLink ← ``(Doc.Inline.other (Inline.errorExplanationLink $(quote name))
+        #[Doc.Inline.other (Inline.errorExplanationShortName $(quote name)) #[]])
       let summary ← ``(Doc.Inline.text $(quote explan.metadata.summary))
       let since ← ``(Doc.Inline.text $(quote explan.metadata.sinceVersion))
       #[nameLink, summary, sev, since]
@@ -72,7 +85,8 @@ htmlToc := false
 %%%
 
 This section provides explanations of errors and warnings that may be generated
-by Lean when processing a source file.
+by Lean when processing a source file. All error names listed below have the
+`lean` package prefix.
 
 {error_explanation_table}
 

Manual/Meta/ErrorExplanation.lean

@@ -678,6 +678,22 @@ def explanation : PartCommand
     addExplanationBlocksFor config.name.getId
   | _ => Lean.Elab.throwUnsupportedSyntax
 
+/--
+Returns the suffix of `name` as a string containing soft-hyphen characters at reasonable split points.
+-/
+def getBreakableSuffix (name : Name) : Option String := do
+  let suffix ← match name with
+    | .str _ s => s
+    | .num _ n => toString n
+    | .anonymous => none
+  let breakableHtml := softHyphenateIdentifiers.rwText (.text false suffix)
+  htmlText breakableHtml
+where
+  htmlText : Verso.Output.Html → String
+    | .text _ txt => txt
+    | .seq elts => elts.foldl (· ++ htmlText ·) ""
+    | .tag _nm _attrs children => htmlText children
+
 open Verso Doc Elab ArgParse in
 open Lean in
 /-- Renders all error explanations as parts of the current page. -/
@@ -690,10 +706,12 @@ def make_explanations : PartCommand
       let titleBits := #[← ``(Inline.other
         (Inline.errorExplanation $(quote name) $(quote explan.metadata.summary))
         #[Inline.code $(quote titleString)])]
+      let some shortTitleString := getBreakableSuffix name
+        | throwError m!"Found invalid explanation name `{name}` when generating explanations section"
       PartElabM.push {
         titleSyntax := quote (k := `str) titleString,
         expandedTitle := some (titleString, titleBits),
-        metadata := none,
+        metadata := some (← `({ shortTitle := $(quote shortTitleString) })),
         blocks := #[],
         priorParts := #[]
       }