From 99d5a25a9b93796cf2a5a3d966be6a0063838f6d Mon Sep 17 00:00:00 2001
From: Krishna Padmasola <kpadmasola@gmail.com>
Date: Mon, 25 Aug 2025 17:02:43 +0530
Subject: [PATCH 1/4] testing verso changes for inserting placeholder for
 missing toTex

---
 src/verso-manual/VersoManual/Basic.lean | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 2cbf32ff..907a6580 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -1271,8 +1271,9 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getBlock? b.name
       | panic! s!"Unknown block {b.name} while rendering.\n\nKnown blocks: {(← readThe ExtensionImpls).blockDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | TeX.logError s!"Block {b.name} doesn't support TeX"
-        return .empty
+      | --TeX.logError s!"Block {b.name} doesn't support TeX"
+        --return .empty
+        return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Block {b.name}" ]
     impl goI goB id b.data content
   inline go i content := do
     let some id := i.id
@@ -1280,8 +1281,10 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getInline? i.name
       | panic! s!"Unknown inline {i.name} while rendering.\n\nKnown inlines: {(← readThe ExtensionImpls).inlineDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | TeX.logError s!"Inline {i.name} doesn't support TeX"
-        return .empty
+      | --TeX.logError s!"Inline {i.name} doesn't support TeX"
+        -- return .empty
+        -- "\color{red}{Missing toTeX for Manual.keywordOf}".
+        return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Inline {i.name}" ]
     impl go id i.data content
 
 

From 3d9df990639b8834ab102015ecb287a836eab765 Mon Sep 17 00:00:00 2001
From: Krishna Padmasola <kpadmasola@gmail.com>
Date: Mon, 25 Aug 2025 21:03:55 +0530
Subject: [PATCH 2/4] suppress `No more header nesting available` error

---
 src/verso/Verso/Doc/TeX.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean
index 8363d063..39b7b26c 100644
--- a/src/verso/Verso/Doc/TeX.lean
+++ b/src/verso/Verso/Doc/TeX.lean
@@ -41,7 +41,8 @@ def logError [Monad m] (message : String) : TeXT g m Unit := do
 def header [Monad m] (name : TeX) : TeXT g m TeX := do
   let opts ← options
   let some i := opts.headerLevel
-    | logError s!"No more header nesting available at {name.asString}"; return \TeX{\textbf{\Lean{name}}}
+    | --logError s!"No more header nesting available at {name.asString}";
+      return \TeX{\textbf{\Lean{name}}}
   let header := opts.headerLevels[i]
   pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}"
 

From 0620a1a49f374e891308860a7e3cefdf4ee37b14 Mon Sep 17 00:00:00 2001
From: Krishna Padmasola <kpadmasola@gmail.com>
Date: Tue, 26 Aug 2025 22:35:17 +0530
Subject: [PATCH 3/4] remove commented code

---
 src/verso-manual/VersoManual/Basic.lean | 9 ++-------
 src/verso/Verso/Doc/TeX.lean            | 3 +--
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 907a6580..8e417fb0 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -1271,9 +1271,7 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getBlock? b.name
       | panic! s!"Unknown block {b.name} while rendering.\n\nKnown blocks: {(← readThe ExtensionImpls).blockDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | --TeX.logError s!"Block {b.name} doesn't support TeX"
-        --return .empty
-        return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Block {b.name}" ]
+      | return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Block {b.name}" ]
     impl goI goB id b.data content
   inline go i content := do
     let some id := i.id
@@ -1281,10 +1279,7 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getInline? i.name
       | panic! s!"Unknown inline {i.name} while rendering.\n\nKnown inlines: {(← readThe ExtensionImpls).inlineDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | --TeX.logError s!"Inline {i.name} doesn't support TeX"
-        -- return .empty
-        -- "\color{red}{Missing toTeX for Manual.keywordOf}".
-        return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Inline {i.name}" ]
+      | return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Inline {i.name}" ]
     impl go id i.data content
 
 
diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean
index 39b7b26c..e5388491 100644
--- a/src/verso/Verso/Doc/TeX.lean
+++ b/src/verso/Verso/Doc/TeX.lean
@@ -41,8 +41,7 @@ def logError [Monad m] (message : String) : TeXT g m Unit := do
 def header [Monad m] (name : TeX) : TeXT g m TeX := do
   let opts ← options
   let some i := opts.headerLevel
-    | --logError s!"No more header nesting available at {name.asString}";
-      return \TeX{\textbf{\Lean{name}}}
+    | return \TeX{\textbf{\Lean{name}}}
   let header := opts.headerLevels[i]
   pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}"
 

From 66f790f206e367c8f97193ab6ba4fb3d9ce97476 Mon Sep 17 00:00:00 2001
From: Krishna Padmasola <kpadmasola@gmail.com>
Date: Thu, 28 Aug 2025 11:37:30 +0530
Subject: [PATCH 4/4] address review comments

---
 src/verso-manual/VersoManual/Basic.lean | 6 ++++--
 src/verso/Verso/Doc/TeX.lean            | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 8e417fb0..ee72b09f 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -1271,7 +1271,8 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getBlock? b.name
       | panic! s!"Unknown block {b.name} while rendering.\n\nKnown blocks: {(← readThe ExtensionImpls).blockDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Block {b.name}" ]
+      | TeX.logError s!"Block {b.name} doesn't support TeX"
+        return \TeX{\textcolor{"red"}{s!"Missing toTeX for Block {b.name}"}}
     impl goI goB id b.data content
   inline go i content := do
     let some id := i.id
@@ -1279,7 +1280,8 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     let some descr := (← readThe ExtensionImpls).getInline? i.name
       | panic! s!"Unknown inline {i.name} while rendering.\n\nKnown inlines: {(← readThe ExtensionImpls).inlineDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
-      | return .command "textcolor" #[] #[ .raw "red", .raw s!"Missing toTeX for Inline {i.name}" ]
+      | TeX.logError s!"Inline {i.name} doesn't support TeX"
+        return \TeX{\textcolor{"red"}{s!"Missing toTeX for Inline {i.name}"}}
     impl go id i.data content
 
 
diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean
index e5388491..0387d546 100644
--- a/src/verso/Verso/Doc/TeX.lean
+++ b/src/verso/Verso/Doc/TeX.lean
@@ -41,7 +41,8 @@ def logError [Monad m] (message : String) : TeXT g m Unit := do
 def header [Monad m] (name : TeX) : TeXT g m TeX := do
   let opts ← options
   let some i := opts.headerLevel
-    | return \TeX{\textbf{\Lean{name}}}
+    | logError s!"No more header nesting available at {name.asString}"
+      return \TeX{\textcolor{"red"}{s!"Header nesting limit reached at {name.asString}"}}
   let header := opts.headerLevels[i]
   pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}"