From c3faad173097ab97156de854ec267711a5dff0a1 Mon Sep 17 00:00:00 2001
From: Max Taldykin <jorpic@gmail.com>
Date: Fri, 3 Mar 2023 15:48:48 +0400
Subject: [PATCH] help break_within to split names at `.`

---
 DocGen4/Output/Base.lean     | 15 ++++++++++++++-
 DocGen4/Output/Module.lean   | 11 +++++------
 DocGen4/Output/Template.lean |  2 +-
 3 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index d664866..eb29fc0 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -174,12 +174,25 @@ def declNameToInkLink (name : Name) : HtmlM String := do
   let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
   return (← moduleNameToInkLink module) ++ "#" ++ name.toString
 
+/--
+Returns a name splitted into parts.
+Together with "break_within" CSS class this helps browser to break a name
+nicely.
+-/
+def breakWithin (name: String) : (Array Html) :=
+  name.splitOn "."
+    |> .map (fun (s: String) => <span class="name">{s}</span>)
+    |> .intersperse "."
+    |> List.toArray
+
 /--
 Returns the HTML doc-gen4 link to a declaration name with "break_within"
 set as class.
 -/
 def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
-  return <a class="break_within" href={← declNameToLink name}>{name.toString}</a>
+  return <a class="break_within" href={← declNameToLink name}>
+      [breakWithin name.toString]
+    </a>
 
 /--
 In Lean syntax declarations the following pattern is quite common:
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 3437bd2..dd673e5 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -66,10 +66,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
   nodes := nodes.push
     <span class="decl_name">
-      <a class="break_within" href={← declNameToLink doc.getName}>
-        -- TODO: HTMLify the name
-        {doc.getName.toString}
-      </a>
+      {← declNameToHtmlBreakWithinLink doc.getName}
     </span>
   for arg in doc.getArgs do
     nodes := nodes.push (← argToHtml arg)
@@ -160,7 +157,9 @@ def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := d
 
 def declarationToNavLink (module : Name) : Html :=
   <div class="nav_link">
-    <a class="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
+    <a class="break_within" href={s!"#{module.toString}"}>
+      [breakWithin module.toString]
+    </a>
   </div>
 
 /--
@@ -184,7 +183,7 @@ Render the internal nav bar (the thing on the right on all module pages).
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
   pure
     <nav class="internal_nav">
-      <h3><a class="break_within" href="#top">{moduleName.toString}</a></h3>
+      <h3><a class="break_within" href="#top">[breakWithin moduleName.toString]</a></h3>
       <p class="gh_nav_link"><a href={← getSourceUrl moduleName none}>source</a></p>
       <div class="imports">
         <details>
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index a77343a..192fb4b 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -44,7 +44,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
 
         <header>
           <h1><label for="nav_toggle"></label>Documentation</h1>
-          <p class="header_filename break_within">{title}</p>
+          <p class="header_filename break_within">[breakWithin title]</p>
           <form action="https://google.com/search" method="get" id="search_form">
             <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
             <input type="text" name="q" autocomplete="off"/>&#32;