From a6bef73a86bfdd2d8c7a1652f7756066771c902f Mon Sep 17 00:00:00 2001
From: fresheed <ok.john.rus@gmail.com>
Date: Thu, 16 Jul 2026 15:23:12 +0200
Subject: [PATCH] added separate styling for Lean comments

---
 BookGenMain.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/BookGenMain.lean b/BookGenMain.lean
index bf7f34b..0678d99 100644
--- a/BookGenMain.lean
+++ b/BookGenMain.lean
@@ -81,10 +81,21 @@ where
     | .para .. | .code .. => pure ()
 
 
+/-- Overrides Verso's default styling, which lumps comments in with numbers,
+punctuation, etc. under the generic code color. -/
+def extraStyle : String := "
+.hl.lean .comment {
+  color: #6a9955;
+  font-style: italic;
+}
+"
+
+open Verso.Output.Html in
 def config : RenderConfig where
   emitTeX := false
   emitHtmlSingle := .no
   emitHtmlMulti := .immediately
   htmlDepth := 1
+  extraHead := #[{{<style>{{Verso.Output.Html.text false extraStyle}}</style>}}]
 
 def main := manualMain (%doc IrisTutorialBook) (extraSteps := [buildExercises]) (config := config)