diff --git a/examples/anchor-examples/AnchorExamples.lean b/examples/anchor-examples/AnchorExamples.lean
index 6863cb386..35a04b8ba 100644
--- a/examples/anchor-examples/AnchorExamples.lean
+++ b/examples/anchor-examples/AnchorExamples.lean
@@ -9,7 +9,10 @@ import AnchorExamples.Basic
 -- ANCHOR: t
 def someTree : Tree Nat :=
 -- ANCHOR: tDef
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 -- ANCHOR_END: tDef
 -- ANCHOR_END: t
 
@@ -25,7 +28,8 @@ deriving instance Repr for Tree
 
 
 -- ANCHOR: proof1
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl
@@ -37,7 +41,8 @@ theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
 
 -- ANCHOR: proof2
 -- Show more tactic combinators and placement of proof states
-theorem Tree.flip_flip_id' (t : Tree α) : t.flip.flip = t := by
+theorem Tree.flip_flip_id' (t : Tree α) :
+    t.flip.flip = t := by
   induction t
   case leaf => rfl
   next l v r ih1 ih2 =>
diff --git a/examples/anchor-examples/lake-manifest.json b/examples/anchor-examples/lake-manifest.json
index d400e8c08..4584d62b9 100644
--- a/examples/anchor-examples/lake-manifest.json
+++ b/examples/anchor-examples/lake-manifest.json
@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",
diff --git a/examples/documented-package/lake-manifest.json b/examples/documented-package/lake-manifest.json
index 4ef6024fd..70f0285ca 100644
--- a/examples/documented-package/lake-manifest.json
+++ b/examples/documented-package/lake-manifest.json
@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",
diff --git a/examples/textbook/DemoTextbook.lean b/examples/textbook/DemoTextbook.lean
index 978badf60..17f5eab3f 100644
--- a/examples/textbook/DemoTextbook.lean
+++ b/examples/textbook/DemoTextbook.lean
@@ -24,7 +24,6 @@ open DemoTextbook
 set_option pp.rawOnError true
 
 
-
 #doc (Manual) "A Textbook" =>
 
 %%%
diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json
index d400e8c08..4584d62b9 100644
--- a/examples/website-examples/lake-manifest.json
+++ b/examples/website-examples/lake-manifest.json
@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",
diff --git a/examples/website-literate/lake-manifest.json b/examples/website-literate/lake-manifest.json
index 839f5daef..92084b86a 100644
--- a/examples/website-literate/lake-manifest.json
+++ b/examples/website-literate/lake-manifest.json
@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",
diff --git a/examples/website/DemoSite/Blog/AnchorBased.lean b/examples/website/DemoSite/Blog/AnchorBased.lean
index de5e053b1..839943c5b 100644
--- a/examples/website/DemoSite/Blog/AnchorBased.lean
+++ b/examples/website/DemoSite/Blog/AnchorBased.lean
@@ -35,12 +35,18 @@ Here's a tree:
 
 ```anchor t
 def someTree : Tree Nat :=
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 ```
 
 And here's just part of its definition:
 ```anchor tDef
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 ```
 
 It's left branch is {anchorTerm tDef}`.branch .leaf 1 .leaf` which includes a reference to {anchorName tDef}`.leaf`.
@@ -58,7 +64,8 @@ Tree.branch
 
 As does proofs and parts of proofs:
 ```anchor proof1
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl
@@ -77,7 +84,8 @@ branch l v r ih1 ih2
 
 This rendering of the same proof doesn't have proof states:
 ```anchor proof1 (showProofStates := false)
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl
diff --git a/examples/website/DemoSite/Blog/Conditionals.lean b/examples/website/DemoSite/Blog/Conditionals.lean
index 77bf5ecf9..c180e7abb 100644
--- a/examples/website/DemoSite/Blog/Conditionals.lean
+++ b/examples/website/DemoSite/Blog/Conditionals.lean
@@ -179,35 +179,43 @@ theorem grow_10_id {α} : grow (α := α) 6 = id := by
 
 Here is a proof with big terms in the context:
 ```lean demo
+section
+open Lean
 
-open Lean in
-def quotedStx [Monad m] [MonadQuotation m] [MonadRef m] (str : String) : m Syntax := do
+variable [Monad m] [MonadQuotation m] [MonadRef m]
+
+def quoted (str : String) : m Syntax := do
   let s ← `(a b c #[x, $(quote str), z])
   pure s
 
-open Lean in
-example [Monad m] [MonadQuotation m] [MonadRef m] : ¬(quotedStx (m := m) = fun (x : String) => pure .missing) := by
-  unfold quotedStx
+example : ¬(quoted (m := m) = fun x => pure .missing) := by
+  unfold quoted
   intro h
   let g : String → m Syntax := fun str => do
     let s ← `(a b c #[x, $(quote str), z])
     pure s
   have : g "hello" ≠ pure .missing := by skip; sorry
   sorry
+
+end
 ```
 
 It's possible to render a lot of info on one example:
 ```lean demo
-elab "%much_info(" t:term ")" : term => open Lean Elab Term in do
+open Lean Elab Term in
+elab "%much_info(" t:term ")" : term => do
   for i in [0:20] do
     logInfoAt t m!"Hello! ({i})"
   logInfoAt t "Some multi-line\ninfo too"
   elabTerm t none
 
-elab "%more_info(" t:term ")" : term => open Lean Elab Term in do
+open Lean Elab Term in
+elab "%more_info(" t:term ")" : term => do
   for i in [0:20] do
     logInfoAt t m!"Hello again! ({i})"
-  logErrorAt t "And a great big error, much wider than the other info!"
+  logErrorAt t <|
+    "And a great big error, " ++
+    "much wider than the other info!"
   elabTerm t none
 ```
 
diff --git a/examples/website/DemoSiteMain.lean b/examples/website/DemoSiteMain.lean
index edbc44e81..a50e1449e 100644
--- a/examples/website/DemoSiteMain.lean
+++ b/examples/website/DemoSiteMain.lean
@@ -32,7 +32,10 @@ def theme : Theme := { Theme.default with
     return {{
       <html>
         <head>
-          <meta charset="UTF-8"/>
+          <meta charset="utf-8"/>
+          <meta name="viewport" content="width=device-width, initial-scale=1"/>
+          <meta name="color-scheme" content="light dark"/>
+          <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/sakura.css/css/sakura.css" type="text/css"/>
           <title>{{ (← param (α := String) "title") }} " — Verso "</title>
           <link rel="stylesheet" href="/static/style.css"/>
           {{← builtinHeader }}
@@ -40,17 +43,17 @@ def theme : Theme := { Theme.default with
         <body>
           <header>
             <div class="inner-wrap">
-            <a class="logo" href="/"><img src="/static/logo.png"/></a>
+            <a class="logo" href="/"><h1>"A Verso Site"</h1></a>
             {{ ← topNav }}
             </div>
           </header>
-          <div class="main" role="main">
+          <main>
             <div class="wrap">
               {{ (← param "content") }}
               {{ postList }}
               {{ catList }}
             </div>
-          </div>
+          </main>
         </body>
       </html>
     }}
diff --git a/examples/website/static_files/style.css b/examples/website/static_files/style.css
index 7ea92db04..31501a46b 100644
--- a/examples/website/static_files/style.css
+++ b/examples/website/static_files/style.css
@@ -1,88 +1,19 @@
 
-/* http://meyerweb.com/eric/tools/css/reset/
-   v2.0 | 20110126
-   License: none (public domain)
-*/
-
-html, body, div, span, applet, object, iframe,
-h1, h2, h3, h4, h5, h6, p, blockquote, pre,
-a, abbr, acronym, address, big, cite, code,
-del, dfn, em, img, ins, kbd, q, s, samp,
-small, strike, strong, sub, sup, tt, var,
-b, u, i, center,
-dl, dt, dd, ol, ul, li,
-fieldset, form, label, legend,
-table, caption, tbody, tfoot, thead, tr, th, td,
-article, aside, canvas, details, embed,
-figure, figcaption, footer, header, hgroup,
-menu, nav, output, ruby, section, summary,
-time, mark, audio, video {
-    margin: 0;
-    padding: 0;
-    border: 0;
-    font-size: 100%;
-    font: inherit;
-    vertical-align: baseline;
-}
-/* HTML5 display-role reset for older browsers */
-article, aside, details, figcaption, figure,
-footer, header, hgroup, menu, nav, section {
-    display: block;
-}
-body {
-    line-height: 1;
-    font-size: 14px;
-}
-/***********************************/
-
-li {
-    margin-left: 1.5em;
-}
-
-pre {
-    font-family: monospace;
-}
-
-p, pre, code.block {
-    line-height: 1.25;
-}
-
-h1 {
-    font-size: 150%;
-}
-
-h2 {
-    font-size: 140%;
-}
-
-h3 {
-    font-size: 130%;
-}
-
-h4 {
-    font-size: 120%;
-}
-
-h5 {
-    font-size: 110%;
-}
-
-h6 {
-    font-size: 105%;
-}
-
-header, div.main {
-    margin-left: 4em;
-    margin-right: 4em;
-    max-width: 50em;
-}
+/**************************/
 
-header {
-    margin-bottom: 1.5em;
+nav ol {
+  display: flex;
+  flex-wrap: wrap; /* Wrap to new lines on small screens */
+  list-style: none;
+  margin: 0;
+  padding: 0;
+  gap: 3rem;
 }
 
-.main p, .main pre, .main code.block {
-  margin-bottom: 0.5em;
+@media (max-width: 600px) {
+  nav ol {
+    flex-direction: column; /* Stack vertically on mobile */
+  }
 }
 
 div.metadata {
@@ -154,6 +85,12 @@ code {
 
 /**************************/
 
+.hl.lean.block {
+  margin-bottom: 2.5rem; /* Match sakura.css's setting for block elements */
+}
+
+/**************************/
+
 .lexed.json .brace {
     color: #0000aa;
 }
diff --git a/lake-manifest.json b/lake-manifest.json
index c8a6c630c..ca984a616 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+   "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 5a45b574b..5b49b11bd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,10 +12,15 @@ lean_lib VersoUtil where
   srcDir := "src/verso-util"
   roots := #[`VersoUtil]
 
+input_file versoVars where
+  text := true
+  path := "static-web/verso-vars.css"
+
 @[default_target]
 lean_lib Verso where
   srcDir := "src/verso"
   roots := #[`Verso]
+  needs := #[versoVars]
 
 @[default_target]
 lean_lib MultiVerso where
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 90153570c..9df4701cf 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/src/verso-blog/VersoBlog.lean
@@ -31,6 +31,7 @@ open Verso ArgParse Doc Elab
 open Verso.SyntaxUtils (parserInputString)
 
 open SubVerso.Examples (loadExamples Example)
+open SubVerso.Examples.Messages (messagesMatch)
 open SubVerso.Module (ModuleItem)
 
 def classArgs : ArgParse DocElabM String := .named `«class» .string false
@@ -764,7 +765,7 @@ where
     pure <| withNewline <| head ++ (← message.data.toString)
 
   mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool :=
-    ws.apply s1.trim == ws.apply s2.trim
+    messagesMatch (ws.apply s1.trim) (ws.apply s2.trim)
 
 open Lean Elab Command in
 elab "define_lexed_text" blockName:ident " ← " lexerName:ident : command => do
diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean
index 430ae5ae1..52ab98657 100644
--- a/src/verso-blog/VersoBlog/Template.lean
+++ b/src/verso-blog/VersoBlog/Template.lean
@@ -14,6 +14,7 @@ import VersoBlog.Basic
 import VersoBlog.Site
 import VersoBlog.Component
 import Verso.Output.Html
+import Verso.Output.Html.CssVars
 import Verso.Code
 
 open Std (HashSet)
@@ -149,7 +150,7 @@ def blockHtml (g : Genre)
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
     hls.blockHtml (toString contextName) (g := g)
   | .message summarize msg, _contents => do
-    return {{<pre class="lean-output hl lean">{{← msg.toHtml (g := g)}}</pre>}}
+    return {{<pre class=s!"lean-output hl lean {msg.severity.class}">{{← msg.toHtml (g := g)}}</pre>}}
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
@@ -300,8 +301,11 @@ def param [TypeName α] (key : String) : TemplateM α := do
     if let some v := val.get? (α := α) then return v
     else throw <| .wrongParamType key (TypeName.typeName α)
 
+
 def builtinHeader : TemplateM Html := do
   let mut out := .empty
+  -- These should come first so later stylesheets can easily override them.
+  out := out ++ {{<style>{{«verso-vars.css»}}</style>}}
   for style in (← read).builtInStyles do
     out := out ++ {{<style>"\n"{{.text false style}}"\n"</style>"\n"}}
   for script in (← read).builtInScripts do
diff --git a/src/verso-blog/VersoBlog/Theme.lean b/src/verso-blog/VersoBlog/Theme.lean
index 32a4c94b7..e765f8178 100644
--- a/src/verso-blog/VersoBlog/Theme.lean
+++ b/src/verso-blog/VersoBlog/Theme.lean
@@ -86,9 +86,12 @@ def primary : Template := do
   return {{
     <html>
       <head>
+        <meta charset="utf-8"/>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+        <meta name="color-scheme" content="light dark"/>
+        <link rel="stylesheet" href="https://unpkg.com/mvp.css"/>
         <title>{{← param (α := String) "title"}}</title>
         {{← builtinHeader}}
-        <link rel="stylesheet" href="/static/style.css"/>
       </head>
       <body>
         {{← topNav}}
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 27875985e..492e0fbbb 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -10,6 +10,7 @@ import Verso.Doc.TeX
 import Verso.Doc.Html
 import Verso.Output.TeX
 import Verso.Output.Html
+import Verso.Output.Html.CssVars
 import Verso.Output.Html.KaTeX
 import Verso.Output.Html.ElasticLunr
 import Verso.Doc.Lsp
@@ -564,6 +565,8 @@ where
       for e in errs do logError e
       pure <| items.map (·.toHtml)
     emitXrefs toc dir state config
+    IO.FS.withFile (dir.join "verso-vars.css") .write fun h => do
+      h.putStrLn Html.«verso-vars.css»
     IO.FS.withFile (dir.join "book.css") .write fun h => do
       h.putStrLn Html.Css.pageStyle
     for (src, dest) in config.extraFiles do
@@ -628,6 +631,8 @@ where
       if let some alt := text.metadata.bind (·.shortTitle) then
         alt
       else titleHtml
+    IO.FS.withFile (root.join "verso-vars.css") .write fun h => do
+      h.putStrLn Html.«verso-vars.css»
     IO.FS.withFile (root.join "book.css") .write fun h => do
       h.putStrLn Html.Css.pageStyle
     for (src, dest) in config.extraFiles do
diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean
index 42198652e..c51a90ee2 100644
--- a/src/verso-manual/VersoManual/Html.lean
+++ b/src/verso-manual/VersoManual/Html.lean
@@ -534,7 +534,8 @@ def page
         <meta charset="utf-8"/>
         <meta name="viewport" content="height=device-height, width=device-width, initial-scale=1, minimum-scale=1, maximum-scale=1"/>
         <title>{{textTitle}}</title>
-        <link rel="stylesheet" href="/book.css" />
+        <link rel="stylesheet" href="book.css" />
+        <link rel="stylesheet" href="verso-vars.css" />
         <script>s!"const __versoSiteRoot = document.baseURI;"</script>
         <script src="https://cdn.jsdelivr.net/npm/marked@11.1.1/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>
         <script src="-verso-search/elasticlunr.min.js"></script>
diff --git a/src/verso-manual/VersoManual/Html/Style.lean b/src/verso-manual/VersoManual/Html/Style.lean
index b49490886..bbcf3ba80 100644
--- a/src/verso-manual/VersoManual/Html/Style.lean
+++ b/src/verso-manual/VersoManual/Html/Style.lean
@@ -11,12 +11,6 @@ def pageStyle : String := r####"
 
 :root {
     /** Typography **/
-    /* The font family used for headers, ToC entries, etc */
-    --verso-structure-font-family: "Helvetica Neue","Segoe UI", "Roboto", Arial,sans-serif;
-    /* The font family used for body text */
-    --verso-text-font-family: "Helvetica Neue","Segoe UI", "Roboto", Arial,sans-serif;
-    /* The font family used for code */
-    --verso-code-font-family: monospace;
     /* What's the maximum line width, for legibility? */
     --verso-content-max-width: 47rem;
     /* Desktop font size */
@@ -24,9 +18,6 @@ def pageStyle : String := r####"
     /* Mobile font size */
     --verso-mobile-font-size: 16px;
 
-    /** Text colors **/
-    --verso-text-color: black;
-
     /** Header appearance **/
     --verso-header-height: 3rem;
     /* Height of the displayed logo **/
@@ -42,9 +33,6 @@ def pageStyle : String := r####"
     /* How wide should the ToC be on non-mobile? */
     --verso-toc-width: 18rem;
 
-    /** Selected items (e.g. search results) */
-    --verso-selected-color: #def;
-
     /** Variables that control the “burger menu” appearance **/
     --verso-burger-height: 1.25rem;
     --verso-burger-width: 1.25rem;
@@ -60,9 +48,6 @@ def pageStyle : String := r####"
     --verso-mobile-burger-width: 1.5rem;
     --verso-mobile-burger-line-width: 0.3rem;
     --verso-mobile-burger-line-radius: 0.3rem;
-
-    /* Colors */
-    --verso-warning-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */
 }
 
 /******** Global parameters not intended for customization by themes ********/
diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
index 93f5b92a2..1c847e1b1 100644
--- a/src/verso/Verso/Code/Highlighted.lean
+++ b/src/verso/Verso/Code/Highlighted.lean
@@ -468,7 +468,7 @@ partial defmethod Highlighted.MessageContents.toHtml (maxTraceDepth : Nat) (expr
         let cs ← children.mapM (·.toHtml (maxTraceDepth - 1) exprHtml)
         pure {{<ul class="trace-children">{{cs.map ({{<li>{{·}}</li>}})}}</ul>}}
       if children.size > 0 then return {{
-        <details class="trace" {{if collapsed then #[] else #[("open", "open")]}}><summary><span class="trace-class">s!"[{cls}]"</span> " " {{msgHtml}}</summary>{{childHtml}}</details>
+        <details class="trace" role="group" {{if collapsed then #[] else #[("open", "open")]}}><summary><span class="trace-class">s!"[{cls}]"</span> " " {{msgHtml}}</summary>{{childHtml}}</details>
       }} else return {{
         <span class="trace"><span class="trace-class">s!"[{cls}]"</span> " " {{msgHtml}}</span>
       }}
@@ -578,17 +578,39 @@ def highlightingStyle : String := "
   white-space: pre;
   font-weight: normal;
   font-style: normal;
+  font-size: inherit;
 }
 
 .hl.lean .keyword {
-  font-weight : bold;
+  color: var(--verso-code-keyword-color,);
+  font-weight: var(--verso-code-keyword-weight, bold);
+  font-style: var(--verso-code-keyword-style, normal);
+  font-family: var(--verso-code-keyword-font-family,);
+}
+
+.hl.lean .const {
+  color: var(--verso-code-const-color,);
+  font-weight: var(--verso-code-const-weight, normal);
+  font-style: var(--verso-code-const-style, normal);
+  font-family: var(--verso-code-const-font-family,);
 }
 
 .hl.lean .var {
-  font-style: italic;
+  color: var(--verso-code-var-color,);
+  font-weight: var(--verso-code-var-weight, normal);
+  font-style: var(--verso-code-var-style, italic);
+  font-family: var(--verso-code-var-font-family,);
+
   position: relative;
 }
 
+.hl.lean .literal, .hl.lean .unknown {
+  color: var(--verso-code-color,);
+  font-weight: normal;
+  font-style: normal;
+  font-family: var(--verso-code-font-family,);
+}
+
 .hover-container {
   width: 0;
   height: 0;
@@ -616,7 +638,6 @@ def highlightingStyle : String := "
   border: 1px solid black;
   padding: 0.5rem;
   z-index: 300;
-  font-size: inherit;
 }
 
 .hl.lean .hover-info.messages {
@@ -630,6 +651,8 @@ def highlightingStyle : String := "
 
 .hl.lean .hover-info code {
   white-space: pre-wrap;
+  background: none;
+  color: black;
 }
 
 .hl.lean .hover-info.messages > code {
@@ -650,6 +673,9 @@ def highlightingStyle : String := "
   margin-top: 0rem;
 }
 
+.hl.lean {
+}
+
 .hl.lean.block {
   display: block;
 }
@@ -659,6 +685,9 @@ def highlightingStyle : String := "
   white-space: pre-wrap;
 }
 
+.hl.lean * {
+}
+
 .hl.lean .token {
   transition: all 0.25s; /* Slight fade for highlights */
 }
@@ -709,12 +738,16 @@ def highlightingStyle : String := "
   border: none;
 }
 
-.error .verso-message {
-    color: red;
+.error .verso-message, .error .verso-message .token, .error .verso-message label {
+  color: var(--verso-error-color);
+}
+
+.error .verso-message .case-label:has(input[type=\"checkbox\"])::before {
+  background-color: var(--verso-error-color) !important;
 }
 
 .hl.lean .has-info.warning :not(.tactic-state):not(.tactic-state *) {
-  text-decoration-color: var(--verso-warning-color);
+  text-decoration-color: var(--verso-warning-indicator-color);
 }
 
 @media (hover: hover) {
@@ -727,6 +760,25 @@ def highlightingStyle : String := "
   background-color: var(--verso-warning-color);
 }
 
+.lean-output {
+  border-left: 0.2em solid transparent;
+  padding: 0 0 0 0.5em;
+  border-top-left-radius: 0;
+  border-bottom-left-radius: 0;
+}
+
+.lean-output.error {
+  border-color: var(--verso-error-indicator-color);
+}
+
+.lean-output.information {
+  border-color: var(--verso-info-indicator-color);
+}
+
+.lean-output.warning {
+  border-color: var(--verso-warning-indicator-color);
+}
+
 .hl.lean .hover-info.messages > code.error {
   background-color: #e5e5e5;
   border-left: 0.2rem solid var(--verso-warning-color);
@@ -739,7 +791,7 @@ def highlightingStyle : String := "
 
 
 .hl.lean .has-info.information :not(.tactic-state):not(.tactic-state *) {
-  text-decoration-color: blue;
+  text-decoration-color: var(--verso-info-indicator-color, blue);
 }
 
 @media (hover: hover) {
@@ -749,20 +801,20 @@ def highlightingStyle : String := "
 }
 
 
-.hl.lean .hover-info.messages > code.info {
+.hl.lean .hover-info.messages > code.information {
   background-color: #e5e5e5;
   border-left: 0.2rem solid #4777ff;
 }
 
-.tippy-box[data-theme~='info'] .hl.lean .hover-info.messages > code.info {
+.tippy-box[data-theme~='info'] .hl.lean .hover-info.messages > code.information {
   background: none;
   border: none;
 }
 
 .hl.lean div.docstring {
-  font-family: sans-serif;
+  font-family: var(--verso-text-font-family, sans-serif);
   white-space: normal;
-  max-width: 40rem;
+  max-width: calc(min(40rem, 90vw));
   width: max-content;
 }
 
@@ -853,12 +905,13 @@ def highlightingStyle : String := "
 .hl.lean .tactic > label::after {
   content: \"\";
   border: 1px solid #bbbbbb;
-  border-radius: 1rem;
-  height: 0.25rem;
+  /* These need to be em, not rem, to scale with the font */
+  border-radius: 1em;
+  height: 0.25em;
   vertical-align: middle;
-  width: 0.6rem;
-  margin-left: 0.1rem;
-  margin-right: 0.1rem;
+  width: 0.6em;
+  margin-left: 0.1em;
+  margin-right: 0.1em;
   display: inline-block;
   transition: all 0.5s;
 }
@@ -880,15 +933,60 @@ def highlightingStyle : String := "
 }
 
 .hl.lean .tactic-state .goal + .goal {
-  margin-top: 1.5rem;
+  margin-top: 1.5em;
+}
+
+/*
+Some CSS frameworks customize details/summary in ways not compatible with Verso's output.
+*/
+
+.hl.lean details {
+  display: block !important;
+  margin: 0;
+}
+
+.hl.lean details summary {
+  display: list-item !important;
+  margin: 0;
+}
+
+.hl.lean details summary:focus {
+  outline: none;
+  outline-offset: none;
+  color: inherit;
+}
+
+.hl.lean ul > li {
+  margin-bottom: 0;
+}
+
+.hl.lean details summary::marker {
+  display: inline !important;
+}
+
+.hl.lean details > summary:first-of-type {
+  list-style-type: disclosure-closed;
+  list-style-position: inside;
+}
+
+.hl.lean details[open] > summary:first-of-type {
+  list-style-type: disclosure-open;
+}
+
+.hl.lean details summary::before, .hl.lean details summary::after {
+  content: \"\" !important;
+  background: none;
+  display: none;
 }
 
 .hl.lean .tactic-state summary {
-  margin-left: -0.5rem;
+  /* These need to be em, not rem, to scale with the font */
+  margin-left: -0.5em;
 }
 
 .hl.lean .tactic-state details {
-  padding-left: 0.5rem;
+  /* These need to be em, not rem, to scale with the font */
+  padding-left: 0.5em;
 }
 
 .hl.lean .case-label {
@@ -936,8 +1034,9 @@ def highlightingStyle : String := "
   display: block;
   overflow: hidden;
   transition: max-height 0.1s ease-in;
-  margin-left: 0.5rem;
-  margin-top: 0.1rem;
+  /* These need to be em, not rem, to scale with the font */
+  margin-left: 0.5em;
+  margin-top: 0.1em;
 }
 
 .hl.lean .labeled-case:has(.case-label input[type=\"checkbox\"]:checked) > :not(:first-child) {
@@ -953,6 +1052,7 @@ def highlightingStyle : String := "
 .hl.lean .goal-name {
   font-style: italic;
   font-family: var(--verso-code-font-family);
+  color: inherit;
 }
 
 .hl.lean .hypotheses {
@@ -970,7 +1070,8 @@ def highlightingStyle : String := "
 
 .hl.lean .hypotheses .colon {
   text-align: center;
-  min-width: 1rem;
+  /* This needs to be em, not rem, to scale with the font */
+  min-width: 1em;
 }
 
 .hl.lean .hypotheses .name {
@@ -983,6 +1084,13 @@ def highlightingStyle : String := "
   font-family: var(--verso-code-font-family);
 }
 
+.tippy-box {
+  /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/
+  -webkit-text-size-adjust: 100%;
+  text-size-adjust: 100%;
+
+}
+
 .tippy-box[data-theme~='lean'] {
   background-color: #e5e5e5;
   color: black;
@@ -1088,6 +1196,10 @@ def highlightingStyle : String := "
   margin: 0 0.25em;
 }
 
+.verso-message .trace {
+  display: block;
+}
+
 .verso-message .trace > summary::marker {
   color: var(--verso-text-color);
 }
diff --git a/src/verso/Verso/Output/Html/CssVars.lean b/src/verso/Verso/Output/Html/CssVars.lean
new file mode 100644
index 000000000..f616a911f
--- /dev/null
+++ b/src/verso/Verso/Output/Html/CssVars.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+namespace Verso.Output.Html
+
+/--
+CSS variables used by all genres that should support HTML output.
+-/
+def «verso-vars.css» := include_str "../../../../../static-web/verso-vars.css"
diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
index 665a56c35..e9e7005b8 100644
--- a/src/verso/Verso/Parser.lean
+++ b/src/verso/Verso/Parser.lean
@@ -3121,6 +3121,68 @@ Remaining: "Let's say more!\n\nhello"
 #guard_msgs in
 #eval blocks {} |>.test! ": an excellent idea\n\nLet's say more!\n\nhello"
 
+/--
+info: Failure @91 (⟨6, 0⟩): non-whitespace
+Final stack:
+  [(Verso.Syntax.dl
+    "ul{"
+    [(Verso.Syntax.desc
+      ":"
+      [(Verso.Syntax.text (str "\" \""))
+       (Verso.Syntax.role
+        "{"
+        `ref
+        [(Verso.Syntax.anon
+          (Verso.Syntax.arg_ident `defs))]
+        "}"
+        "["
+        [(Verso.Syntax.text
+          (str "\"Basic definitions\""))]
+        "]")]
+      "=>"
+      [(Verso.Syntax.para
+        "para{"
+        [(Verso.Syntax.text
+          (str "\"The def is something\""))]
+        "}")])
+     (Verso.Syntax.desc
+      ":"
+      [(Verso.Syntax.text (str "\" \""))
+       (Verso.Syntax.role
+        "{"
+        `ref
+        [(Verso.Syntax.anon
+          (Verso.Syntax.arg_ident `large))]
+        "}"
+        "["
+        [(Verso.Syntax.role
+          "{"
+          `Sufficiently
+          [(Verso.Syntax.anon
+            (Verso.Syntax.arg_ident `large))]
+          "}"
+          "["
+          [(Verso.Syntax.footnote <missing>)]
+          "]")]
+        "]")])])]
+Remaining: "\n  More text\n\n: `foo`\n\n  Thing\n"
+-/
+#guard_msgs in
+#eval recoverBlockWith #[.missing] (blocks {}) |>.test!
+": {ref defs}[Basic definitions]
+
+  The def is something
+
+: {ref large}{Sufficiently large}
+
+  More text
+
+: `foo`
+
+  Thing
+"
+
+
 /--
 info: Success! Final stack:
   [(Verso.Syntax.ol
diff --git a/static-web/verso-vars.css b/static-web/verso-vars.css
new file mode 100644
index 000000000..9e3e5914b
--- /dev/null
+++ b/static-web/verso-vars.css
@@ -0,0 +1,55 @@
+:root {
+    /** Typography **/
+    /* The font family used for headers, ToC entries, etc */
+    --verso-structure-font-family: "Helvetica Neue","Segoe UI", "Roboto", Arial,sans-serif;
+    /* The font family used for body text */
+    --verso-text-font-family: "Helvetica Neue","Segoe UI", "Roboto", Arial,sans-serif;
+    /* The font family used for code */
+    --verso-code-font-family: monospace;
+
+    /** Text colors **/
+    --verso-text-color: black;
+    --verso-code-color: black;
+    --verso-structure-color: black;
+
+    /** Selected items (e.g. search results) */
+    --verso-selected-color: #def;
+
+    /** Message colors **/
+    /*
+    These colors are used to render Lean's feedback. They come in three severities and two
+    variants. The raw color itself is used for the text of a message of the indicated severity,
+    while the presence of such a message is indicated using the indicator color (e.g. via a
+    wavy underline or a bar in the margin).
+    */
+    --verso-info-color: black;
+    --verso-info-indicator-color: #4777ff;
+    --verso-warning-color: black;
+    --verso-warning-indicator-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */
+    --verso-error-color: #cc0000;
+    --verso-error-indicator-color: #ff0000;
+
+    /** Code Highlighting **/
+    /*
+    These variables control the rendering of Lean code emitted by Verso. Each category that can be
+    highlighted supports the customization of color, weight, style, and family.
+    */
+    /* Constants (e.g. `List` or `id` or `none`) */
+    --verso-code-const-color: var(--verso-code-color);
+    --verso-code-const-weight: normal;
+    --verso-code-const-style: normal;
+    --verso-code-const-font-family: var(--verso-code-font-family);
+
+    /* Keywords/atoms (e.g. `for` or `def` or `induction`) */
+    --verso-code-keyword-color: var(--verso-code-color);
+    --verso-code-keyword-weight: bold;
+    --verso-code-keyword-style: normal;
+    --verso-code-keyword-font-family: var(--verso-code-font-family);
+
+    /* Local bindings (e.g. `x` in `let x := 5`) */
+    --verso-code-var-color: var(--verso-code-color);
+    --verso-code-var-weight: normal;
+    --verso-code-var-style: italic;
+    --verso-code-kw-font-family: var(--verso-code-font-family);
+
+}