feat: render Markdown docstrings in blogs

leanprover · Jan 3, 2024 · 58747dd · 58747dd
1 parent 6732421
commit 58747dd
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean
@@ -250,6 +250,12 @@ def highlightingStyle : String := "
   background-color: #4777ff;
 }
 
+.hl.lean div.docstring {
+  font-family: sans-serif;
+  white-space: normal;
+  width: 40em;
+}
+
 "
 
 def highlightingJs : String :=
@@ -275,6 +281,15 @@ def highlightingJs : String :=
             }
         });
     }
+    /* Render docstrings */
+    for (const d of document.querySelectorAll(\"pre.docstring\")) {
+        const str = d.innerText;
+        const html = marked.parse(str);
+        const rendered = document.createElement(\"div\");
+        rendered.classList.add(\"docstring\");
+        rendered.innerHTML = html;
+        d.parentNode.replaceChild(rendered, d);
+    }
 }
 "
 

diff --git a/src/leanblog/LeanDoc/Genre/Blog/Template.lean b/src/leanblog/LeanDoc/Genre/Blog/Template.lean
@@ -50,7 +50,7 @@ defmethod Highlighted.Token.Kind.hover? : (tok : Highlighted.Token.Kind) → Opt
   | .const n doc | .keyword (some n) doc =>
     let docs := match doc with
       | none => .empty
-      | some txt => {{<hr/><p>{{txt}}</p>}}
+      | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}
     some <| hover {{ {{toString n}} {{docs}} }}
   | _ => none
 
@@ -208,6 +208,7 @@ def builtinHeader : TemplateM Html := do
   out := out ++ {{
     <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-n8MVd4RsNIU0tAv4ct0nTaAbDJwPJzDEaqSD1odI+WdtXRGWt2kTvGFasHpSy3SV" crossorigin="anonymous"/>
     <script defer="defer" src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-XjKyOOlGwcjNTAIQHIpgOno0Hl1YQqzUOEleOLALmuqehneUG+vnGctmUb0ZY0l8" crossorigin="anonymous"></script>
+    <script src="https://cdn.jsdelivr.net/npm/[email protected]/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>
   }}
 
   pure out