diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index 2cbf32ff..ee72b09f 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -1272,7 +1272,7 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where | 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 \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 @@ -1281,7 +1281,7 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where | 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 + 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 8363d063..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 - | 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{\textcolor{"red"}{s!"Header nesting limit reached at {name.asString}"}} let header := opts.headerLevels[i] pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}"