Skip to content

Commit 31cf223

Browse files
david-christiansendavid-christiansen
authored
fix: small TeX rendering issues (#711)
This fixes some issues found with a user's document: 1. Double escaping of symbols in `\LeanVerb|...|` 2. Hyperref's `\href` has a [bug when pages are spanned](https://tex.stackexchange.com/questions/54136/hyperref-link-spans-a-pagebreak-looks-ugly) 3. A missing Unicode character was mapped to a fallback
1 parent 962af04 commit 31cf223

File tree

6 files changed

+161
-6
lines changed

6 files changed

+161
-6
lines changed

‎src/tests/integration/code-content-doc/expected/tex/main.tex‎

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,38 @@
77

88
\usepackage{fancyvrb}
99
\usepackage{fvextra}
10+
\usepackage{xparse}
1011

1112
\usepackage[most]{tcolorbox}
12-
\usepackage{hyperref}
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}{vm}{%
35+
\ifinfootnote%
36+
#2~(\url{#1})%
37+
\else%
38+
#2\footnote{\url{#1}}%
39+
\fi%
40+
}
41+
1342
\usepackage[normalem]{ulem}
1443
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
1544
\usepackage{newunicodechar}
@@ -19,6 +48,8 @@
1948
% DejaVu Sans Mono Oblique. \textup
2049
% is fontspec for "upright, not italic/oblique".
2150
\newunicodechar{✝}{\textup{✝}}
51+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
52+
\newunicodechar{‑}{-}
2253

2354
\definecolor{errorColor}{HTML}{ff0000}
2455
\definecolor{infoColor}{HTML}{007f00}

‎src/tests/integration/extra-files-doc/expected/tex/main.tex‎

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,38 @@
77

88
\usepackage{fancyvrb}
99
\usepackage{fvextra}
10+
\usepackage{xparse}
1011

1112
\usepackage[most]{tcolorbox}
12-
\usepackage{hyperref}
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}{vm}{%
35+
\ifinfootnote%
36+
#2~(\url{#1})%
37+
\else%
38+
#2\footnote{\url{#1}}%
39+
\fi%
40+
}
41+
1342
\usepackage[normalem]{ulem}
1443
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
1544
\usepackage{newunicodechar}
@@ -19,6 +48,8 @@
1948
% DejaVu Sans Mono Oblique. \textup
2049
% is fontspec for "upright, not italic/oblique".
2150
\newunicodechar{✝}{\textup{✝}}
51+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
52+
\newunicodechar{‑}{-}
2253

2354
\definecolor{errorColor}{HTML}{ff0000}
2455
\definecolor{infoColor}{HTML}{007f00}

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

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,38 @@
77

88
\usepackage{fancyvrb}
99
\usepackage{fvextra}
10+
\usepackage{xparse}
1011

1112
\usepackage[most]{tcolorbox}
12-
\usepackage{hyperref}
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}{vm}{%
35+
\ifinfootnote%
36+
#2~(\url{#1})%
37+
\else%
38+
#2\footnote{\url{#1}}%
39+
\fi%
40+
}
41+
1342
\usepackage[normalem]{ulem}
1443
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
1544
\usepackage{newunicodechar}
@@ -19,6 +48,8 @@
1948
% DejaVu Sans Mono Oblique. \textup
2049
% is fontspec for "upright, not italic/oblique".
2150
\newunicodechar{✝}{\textup{✝}}
51+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
52+
\newunicodechar{‑}{-}
2253

2354
\definecolor{errorColor}{HTML}{ff0000}
2455
\definecolor{infoColor}{HTML}{007f00}

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

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,38 @@
77

88
\usepackage{fancyvrb}
99
\usepackage{fvextra}
10+
\usepackage{xparse}
1011

1112
\usepackage[most]{tcolorbox}
12-
\usepackage{hyperref}
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}{vm}{%
35+
\ifinfootnote%
36+
#2~(\url{#1})%
37+
\else%
38+
#2\footnote{\url{#1}}%
39+
\fi%
40+
}
41+
1342
\usepackage[normalem]{ulem}
1443
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
1544
\usepackage{newunicodechar}
@@ -19,6 +48,8 @@
1948
% DejaVu Sans Mono Oblique. \textup
2049
% is fontspec for "upright, not italic/oblique".
2150
\newunicodechar{✝}{\textup{✝}}
51+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
52+
\newunicodechar{‑}{-}
2253

2354
\definecolor{errorColor}{HTML}{ff0000}
2455
\definecolor{infoColor}{HTML}{007f00}

‎src/verso-manual/VersoManual/TeX.lean‎

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,38 @@ r##"
1616
1717
\usepackage{fancyvrb}
1818
\usepackage{fvextra}
19+
\usepackage{xparse}
1920
2021
\usepackage[most]{tcolorbox}
21-
\usepackage{hyperref}
22+
23+
% Detect whether we're in a footnote. This is used later to avoid \href rendering bugs.
24+
\newif\ifinfootnote
25+
\infootnotefalse
26+
27+
\let\oldfootnote\footnote
28+
\renewcommand{\footnote}[1]{%
29+
\oldfootnote{\infootnotetrue#1\infootnotefalse}%
30+
}
31+
32+
\let\oldfootnotetext\footnotetext
33+
\renewcommand{\footnotetext}[1]{%
34+
\oldfootnotetext{\infootnotetrue#1\infootnotefalse}%
35+
}
36+
37+
\usepackage[breaklinks=true, hyperfootnotes=false]{hyperref}
38+
39+
% Redefines \href to show footnotes with URLs instead. This works around a page breaking bug in
40+
% hyperref and also makes the link useful on paper. If already in a footnote, the URL is
41+
% in parentheses instead.
42+
\let\oldhref\href
43+
\RenewDocumentCommand{\href}{vm}{%
44+
\ifinfootnote%
45+
#2~(\url{#1})%
46+
\else%
47+
#2\footnote{\url{#1}}%
48+
\fi%
49+
}
50+
2251
\usepackage[normalem]{ulem}
2352
\newcommand{\coloredwave}[2]{\textcolor{#1}{\uwave{\textcolor{black}{#2}}}}
2453
\usepackage{newunicodechar}
@@ -28,6 +57,8 @@ r##"
2857
% DejaVu Sans Mono Oblique. \textup
2958
% is fontspec for "upright, not italic/oblique".
3059
\newunicodechar{✝}{\textup{✝}}
60+
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
61+
\newunicodechar{‑}{-}
3162
3263
\definecolor{errorColor}{HTML}{ff0000}
3364
\definecolor{infoColor}{HTML}{007f00}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ public partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → Te
131131
pure \TeX{\emph{\Lean{← content.mapM toTeX}}}
132132
| .bold content => do
133133
pure \TeX{\textbf{\Lean{← content.mapM toTeX}}}
134-
| .code str => verbatimInline (escapeForVerbatim str)
134+
| .code str => verbatimInline (.raw <| escapeForVerbatim str)
135135
| .math .inline str => pure <| .raw s!"${str}$"
136136
| .math .display str => pure <| .raw s!"\\[{str}\\]"
137137
| .concat inlines => inlines.mapM toTeX

0 commit comments

Comments
 (0)