Skip to content

Commit 4a3ee22

Browse files
robsimmonsrobsimmons
authored
fix: add braces to item description to avoid errors on ] (leanprover#900)
In writing leanprover#876, @david-christiansen noted "this branch encountered a bug in the TeX code generation that needed fixing" — but I think the issue was slightly misdiagnosed, it wasn't a fragility issue, a `]` anywhere in an item description (including outside of verbatim) caused a rendering issue because it was read as the description closer. This fix fixes the bug from leanprover#876, also fixes bugs for `]` in literal text, and adds a test for the behavior.
1 parent f44606d commit 4a3ee22

5 files changed

Lines changed: 217 additions & 5 deletions

File tree

‎src/tests/TestMain.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -362,6 +362,7 @@ def tests := [
362362
testTexOutput "extra-files-doc" ExtraFilesDoc.doc
363363
(extraFiles := [("src/tests/integration/extra-files-doc/test-data/shared", "shared")])
364364
(extraFilesTeX := [("src/tests/integration/extra-files-doc/test-data/TeX-only", "TeX-only")]),
365+
testTexOutput "escape-doc" Escape.doc,
365366
testTexOutput "front-matter-doc" FrontMatter.doc,
366367
testTexOutput "diagram-doc" DiagramDoc.doc,
367368
testZip,

‎src/tests/Tests.lean‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,14 @@ import Tests.InlineStringPositions
1717
import Tests.Integration
1818
import Tests.Integration.SampleDoc
1919
import Tests.Integration.CodeContent
20+
import Tests.Integration.DiagramDoc
21+
import Tests.Integration.Escape
2022
import Tests.Integration.ExtraFilesDoc
21-
import Tests.LeanCode
22-
import Tests.Linters
23-
import Tests.Integration.InheritanceDoc
2423
import Tests.Integration.FrontMatter
24+
import Tests.Integration.InheritanceDoc
2525
import Tests.Integration.LeanSection
26-
import Tests.Integration.DiagramDoc
26+
import Tests.LeanCode
27+
import Tests.Linters
2728
import Tests.Method
2829
import Tests.NestedTacticHtml
2930
import Tests.ParserRegression

‎src/tests/Tests/Integration/Escape.lean‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Author: Rob Simmons
5+
-/
6+
import Verso
7+
import VersoManual
8+
9+
namespace Verso.Integration.Escape
10+
11+
open Verso Genre Manual InlineLean
12+
13+
--------------------
14+
15+
#docs (Manual) doc "Some code" :=
16+
:::::::
17+
18+
%%%
19+
authors := ["A robot"]
20+
%%%
21+
22+
We need to check that closed braces (`]`) can appear inside item descriptions.
23+
24+
: As regular text: \]
25+
26+
lorum ipsum \]
27+
28+
: As code: `]`
29+
30+
* a `]`
31+
* b
32+
* c
33+
34+
: As math: $`]`
35+
36+
lorum ipsum $`]`
37+
38+
39+
1. fish
40+
2. fruit
41+
3. bat
42+
43+
:::::::

‎src/tests/integration/escape-doc/expected/tex/main.tex‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
2+
\documentclass{memoir}
3+
4+
\usepackage{sourcecodepro}
5+
\usepackage{sourcesanspro}
6+
\usepackage{sourceserifpro}
7+
8+
\usepackage{fancyvrb}
9+
\usepackage{fvextra}
10+
\usepackage{xparse}
11+
12+
\usepackage[most]{tcolorbox}
13+
14+
% Detect whether we're in a footnote. This is used later to avoid \href rendering bugs.
15+
\newif\ifinfootnote
16+
\infootnotefalse
17+
18+
\let\oldfootnote\footnote
19+
\renewcommand{\footnote}[1]{%
20+
\oldfootnote{\infootnotetrue#1\infootnotefalse}%
21+
}
22+
23+
\let\oldfootnotetext\footnotetext
24+
\renewcommand{\footnotetext}[1]{%
25+
\oldfootnotetext{\infootnotetrue#1\infootnotefalse}%
26+
}
27+
28+
\usepackage[breaklinks=true, hyperfootnotes=false]{hyperref}
29+
30+
% Redefines \href to show footnotes with URLs instead. This works around a page breaking bug in
31+
% hyperref and also makes the link useful on paper. If already in a footnote, the URL is
32+
% in parentheses instead.
33+
\let\oldhref\href
34+
\RenewDocumentCommand{\href}{mm}{%
35+
\ifinfootnote%
36+
#2~(\url{#1})%
37+
\else%
38+
#2\footnote{\url{#1}}%
39+
\fi%
40+
}
41+
42+
\usepackage[normalem]{ulem}
43+
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
44+
\usepackage{newunicodechar}
45+
46+
% Work around the fact that
47+
% U+271D LATIN CROSS doesn't exist in
48+
% DejaVu Sans Mono Oblique. \textup
49+
% is fontspec for "upright, not italic/oblique".
50+
\newunicodechar{✝}{\textup{✝}}
51+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
52+
\newunicodechar{‑}{-}
53+
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
57+
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
58+
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
59+
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
60+
\DefineVerbatimEnvironment{LeanVerbatim}{Verbatim}
61+
{commandchars=\\\{\},fontsize=\small,breaklines=true}
62+
\DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left}
63+
\CustomVerbatimCommand{\LeanVerb}{Verb}
64+
{commandchars=\\\{\},fontsize=\small,breaklines=true}
65+
\CustomVerbatimCommand{\FileListingVerb}{Verb}
66+
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
67+
68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
88+
\definecolor{bordercolor}{HTML}{98B2C0}
89+
\definecolor{medgray}{HTML}{555555}
90+
\newtcolorbox{docstringBox}[2][]{colback=white,
91+
breakable,
92+
colframe=bordercolor,
93+
colbacktitle=white,
94+
enhanced,
95+
coltitle=medgray,
96+
attach boxed title to top left={xshift=2mm,yshift=-2mm},
97+
boxrule=0.4pt,
98+
fonttitle=\sffamily\fontsize{6pt}{7pt}\selectfont,
99+
boxed title style={top=-0.3mm,bottom=-0.3mm,left=-0.3mm,right=-0.3mm,boxrule=0.4pt},
100+
title={#2},#1}
101+
102+
103+
\makechapterstyle{lean}{%
104+
\renewcommand*{\chaptitlefont}{\sffamily\HUGE}
105+
\renewcommand*{\chapnumfont}{\chaptitlefont}
106+
% allow for 99 chapters!
107+
\settowidth{\chapindent}{\chapnumfont 999}
108+
\renewcommand*{\printchaptername}{}
109+
\renewcommand*{\chapternamenum}{}
110+
\renewcommand*{\chapnumfont}{\chaptitlefont}
111+
\renewcommand*{\printchapternum}{%
112+
\noindent\llap{\makebox[\chapindent][l]{%
113+
\chapnumfont \thechapter}}}
114+
\renewcommand*{\afterchapternum}{}
115+
}
116+
117+
\chapterstyle{lean}
118+
119+
\setsecheadstyle{\sffamily\bfseries\Large}
120+
\setsubsecheadstyle{\sffamily\bfseries\large}
121+
\setsubsubsecheadstyle{\sffamily\bfseries}
122+
123+
\renewcommand{\cftchapterfont}{\normalfont\sffamily}
124+
\renewcommand{\cftsectionfont}{\normalfont\sffamily}
125+
\renewcommand{\cftchapterpagefont}{\normalfont\sffamily}
126+
\renewcommand{\cftsectionpagefont}{\normalfont\sffamily}
127+
\setmonofont{DejaVu Sans Mono}
128+
129+
\title{\sffamily Some code}
130+
\author{\sffamily A robot}
131+
\date{\sffamily }
132+
133+
\begin{document}
134+
135+
\frontmatter
136+
137+
\begin{titlingpage}
138+
\maketitle
139+
\end{titlingpage}
140+
141+
\tableofcontents
142+
143+
144+
\cleardoublepage
145+
We need to check that closed braces (\LeanVerb|]|) can appear inside item descriptions.
146+
\begin{description}
147+
\item[{ As regular text: ]}] lorum ipsum ]\item[{ As code: \LeanVerb|]|}] \begin{itemize}
148+
\item a \LeanVerb|]|
149+
\item b
150+
\item c
151+
152+
\end{itemize}
153+
\item[{ As math: $]$}] lorum ipsum $]$\begin{enumerate}
154+
\item fish
155+
\item fruit
156+
\item bat
157+
158+
\end{enumerate}
159+
160+
\end{description}
161+
162+
163+
\mainmatter
164+
\end{document}

‎src/verso/Verso/Doc/TeX.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,10 @@ public partial defmethod Block.toTeX : Block g → TeXT g m TeX
215215
| .ol _start items => do -- TODO start numbering here
216216
pure \TeX{\begin{enumerate} \Lean{← items.mapM fun li => do pure \TeX{\item " " \Lean{← li.contents.mapM Block.toTeX} s!"\n"}}\end{enumerate} }
217217
| .dl items => do
218-
pure \TeX{\begin{description} \Lean{← items.mapM fun li => do pure \TeX{\item[\Lean{← li.term.mapM Inline.toTeX}] " " \Lean{← li.desc.mapM Block.toTeX}}} \end{description} }
218+
pure \TeX{\begin{description} \Lean{← items.mapM fun li => do
219+
-- Protect the item label with curly braces, avoiding an error if it includes a literal `]`
220+
let itemLabel : TeX := .seq (#[.raw "{"] ++ (← li.term.mapM Inline.toTeX) ++ #[.raw "}"])
221+
pure \TeX{\item[\Lean{itemLabel}] " " \Lean{← li.desc.mapM Block.toTeX}}} \end{description} }
219222
| .code content => do
220223
pure \TeX{\begin{verbatim} \Lean{.raw content} \end{verbatim}}
221224
| .concat items => TeX.seq <$> items.mapM Block.toTeX

0 commit comments

Comments
 (0)