Skip to content

Commit 6327265

Browse files
david-christiansendavid-christiansen
authored
feat: split document by front and back matter in TeX (#714)
Before, the content before the first header became \chapter*{Introduction}, but that didn't work well if there was an explicit introduction header. Now it, and the prefix of unnumbered chapters, become \frontmatter, and the suffix of unnumbered chapters become \backmatter.
1 parent 3c5d4b1 commit 6327265

File tree

12 files changed

+293
-16
lines changed

12 files changed

+293
-16
lines changed

‎src/tests/TestMain.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,7 @@ def tests := [
164164
testTexOutput "extra-files-doc" ExtraFilesDoc.doc
165165
(extraFiles := [("src/tests/integration/extra-files-doc/test-data/shared", "shared")])
166166
(extraFilesTeX := [("src/tests/integration/extra-files-doc/test-data/TeX-only", "TeX-only")]),
167+
testTexOutput "front-matter-doc" FrontMatter.doc,
167168
testZip
168169
]
169170

‎src/tests/Tests.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import Tests.Integration.CodeContent
1616
import Tests.Integration.ExtraFilesDoc
1717
import Tests.LeanCode
1818
import Tests.Integration.InheritanceDoc
19+
import Tests.Integration.FrontMatter
1920
import Tests.ParserRegression
2021
import Tests.Paths
2122
import Tests.HtmlEntities

‎src/tests/Tests/Integration.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -50,22 +50,24 @@ partial def copyFiles (pairs : Array (System.FilePath × System.FilePath)) :
5050

5151
/-- Main test runner -/
5252
def runTests (config : Config) : IO Unit := do
53-
unless ← System.FilePath.pathExists config.testDir do
54-
throw <| .userError s!"Test directory not found: {config.testDir}"
55-
5653
let outputRoot := config.testDir / "output"
5754
let expectedRoot := config.testDir / "expected"
5855

5956
if config.updateExpected then
57+
-- Create the test directory if it doesn't exist
58+
unless ← System.FilePath.pathExists config.testDir do
59+
IO.FS.createDirAll config.testDir
6060
unless ← System.FilePath.pathExists outputRoot do
6161
IO.FS.createDirAll outputRoot
62-
config.runTest
62+
config.runTest
6363
let outputFiles := (← filesBelow outputRoot)
6464
IO.println s!"Updating expected outputs in {config.testDir}..."
6565
if ← System.FilePath.pathExists expectedRoot then do
6666
IO.FS.removeDirAll expectedRoot
6767
copyFiles (outputFiles.map (fun p => (outputRoot / p, expectedRoot / p)))
6868
else
69+
unless ← System.FilePath.pathExists config.testDir do
70+
throw <| .userError s!"Test directory not found: {config.testDir}"
6971
unless ← System.FilePath.pathExists expectedRoot do
7072
IO.FS.createDirAll expectedRoot
7173
let expectedFiles := (← filesBelow expectedRoot)

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

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
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: David Thrane Christiansen
5+
-/
6+
import Verso
7+
import VersoManual
8+
9+
namespace Verso.Integration.FrontMatter
10+
11+
open Verso Genre Manual
12+
13+
#docs (Manual) doc "Front Matter Test Document" :=
14+
:::::::
15+
16+
%%%
17+
shortTitle := "FrontMatter"
18+
authors := ["Test Author"]
19+
%%%
20+
21+
This is the introduction text that appears before any chapters.
22+
It should be part of the front matter.
23+
24+
# Preface
25+
%%%
26+
tag := "preface"
27+
number := false
28+
%%%
29+
30+
This is an unnumbered preface section.
31+
It should appear in the front matter, before `\mainmatter`.
32+
33+
# Chapter One
34+
%%%
35+
tag := "ch1"
36+
%%%
37+
38+
This is the first numbered chapter.
39+
It should appear after `\mainmatter`.
40+
41+
# Chapter Two
42+
%%%
43+
tag := "ch2"
44+
%%%
45+
46+
This is the second numbered chapter.
47+
It should also appear after `\mainmatter`.
48+
49+
# Acknowledgments
50+
%%%
51+
tag := "ack"
52+
number := false
53+
%%%
54+
55+
This is an unnumbered acknowledgments section at the end.
56+
It should appear in the back matter, after `\backmatter`.
57+
58+
# Index
59+
%%%
60+
tag := "index"
61+
number := false
62+
%%%
63+
64+
This is an unnumbered index section.
65+
It should also appear in the back matter.
66+
67+
:::::::
68+
69+
end Verso.Integration.FrontMatter

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,9 +120,7 @@
120120

121121
\tableofcontents
122122

123-
\mainmatter
124123

125-
\chapter*{Introduction}
126124
Here is some code with vertical bars:
127125
\begin{LeanVerbatim}
128126
\textbf{def} or := (· \symbol{124}\symbol{124} ·)
@@ -194,4 +192,6 @@ \chapter*{Introduction}
194192

195193
\end{itemize}
196194

195+
196+
\mainmatter
197197
\end{document}

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,8 +120,9 @@
120120

121121
\tableofcontents
122122

123-
\mainmatter
124123

124+
125+
\mainmatter
125126
\chapter{Testing Extra Files}
126127

127128
This document tests the \LeanVerb|extraFiles|, \LeanVerb|extraFilesHtml|, and \LeanVerb|extraFilesTex| functionality.

‎src/tests/integration/front-matter-doc/expected/tex/main.tex‎

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
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}{ff0000}
55+
\definecolor{infoColor}{HTML}{007f00}
56+
\definecolor{warningColor}{HTML}{0000ff}
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}
65+
\CustomVerbatimCommand{\FileListingVerb}{Verb}
66+
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
67+
68+
\definecolor{bordercolor}{HTML}{98B2C0}
69+
\definecolor{medgray}{HTML}{555555}
70+
\newtcolorbox{docstringBox}[2][]{colback=white,
71+
breakable,
72+
colframe=bordercolor,
73+
colbacktitle=white,
74+
enhanced,
75+
coltitle=medgray,
76+
attach boxed title to top left={xshift=2mm,yshift=-2mm},
77+
boxrule=0.4pt,
78+
fonttitle=\sffamily\fontsize{6pt}{7pt}\selectfont,
79+
boxed title style={top=-0.3mm,bottom=-0.3mm,left=-0.3mm,right=-0.3mm,boxrule=0.4pt},
80+
title={#2},#1}
81+
82+
83+
\makechapterstyle{lean}{%
84+
\renewcommand*{\chaptitlefont}{\sffamily\HUGE}
85+
\renewcommand*{\chapnumfont}{\chaptitlefont}
86+
% allow for 99 chapters!
87+
\settowidth{\chapindent}{\chapnumfont 999}
88+
\renewcommand*{\printchaptername}{}
89+
\renewcommand*{\chapternamenum}{}
90+
\renewcommand*{\chapnumfont}{\chaptitlefont}
91+
\renewcommand*{\printchapternum}{%
92+
\noindent\llap{\makebox[\chapindent][l]{%
93+
\chapnumfont \thechapter}}}
94+
\renewcommand*{\afterchapternum}{}
95+
}
96+
97+
\chapterstyle{lean}
98+
99+
\setsecheadstyle{\sffamily\bfseries\Large}
100+
\setsubsecheadstyle{\sffamily\bfseries\large}
101+
\setsubsubsecheadstyle{\sffamily\bfseries}
102+
103+
\renewcommand{\cftchapterfont}{\normalfont\sffamily}
104+
\renewcommand{\cftsectionfont}{\normalfont\sffamily}
105+
\renewcommand{\cftchapterpagefont}{\normalfont\sffamily}
106+
\renewcommand{\cftsectionpagefont}{\normalfont\sffamily}
107+
\setmonofont{DejaVu Sans Mono}
108+
109+
\title{\sffamily Front Matter Test Document}
110+
\author{\sffamily Test Author}
111+
\date{\sffamily }
112+
113+
\begin{document}
114+
115+
\frontmatter
116+
117+
\begin{titlingpage}
118+
\maketitle
119+
\end{titlingpage}
120+
121+
\tableofcontents
122+
123+
124+
This is the introduction text that appears before any chapters.
125+
It should be part of the front matter.
126+
\chapter{Preface}
127+
128+
This is an unnumbered preface section.
129+
It should appear in the front matter, before \LeanVerb|\symbol{92}mainmatter|.
130+
131+
132+
133+
134+
135+
\mainmatter
136+
\chapter{Chapter One}
137+
138+
This is the first numbered chapter.
139+
It should appear after \LeanVerb|\symbol{92}mainmatter|.
140+
141+
142+
143+
144+
\chapter{Chapter Two}
145+
146+
This is the second numbered chapter.
147+
It should also appear after \LeanVerb|\symbol{92}mainmatter|.
148+
149+
150+
151+
152+
153+
\backmatter
154+
\chapter{Acknowledgments}
155+
156+
This is an unnumbered acknowledgments section at the end.
157+
It should appear in the back matter, after \LeanVerb|\symbol{92}backmatter|.
158+
159+
160+
161+
162+
\chapter{Index}
163+
164+
This is an unnumbered index section.
165+
It should also appear in the back matter.
166+
167+
168+
169+
170+
\end{document}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,11 +120,11 @@
120120

121121
\tableofcontents
122122

123-
\mainmatter
124123

125-
\chapter*{Introduction}
126124
\begin{docstringBox}{structure}
127125
\LeanVerb|Verso.Integration.InheritanceDoc.FooExtends : Type|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|Verso.Integration.InheritanceDoc.FooExtends.mk|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|barField1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|BarExtended|\par \LeanVerb|barField2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|BarExtended|\par \LeanVerb|fooField1| : \LeanVerb|Nat|\par Documentation for fooField1\par \LeanVerb|fooField2| : \LeanVerb|String|\par Documentation for fooField2
128126
\end{docstringBox}
129127

128+
129+
\mainmatter
130130
\end{document}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,13 +120,13 @@
120120

121121
\tableofcontents
122122

123-
\mainmatter
124123

125-
\chapter*{Introduction}
126124
\begin{docstringBox}{def}
127125
\LeanVerb|Verso.Integration.SampleDoc.sample_constant : Type|\tcblower This is a docstring.Here's some more text with a \LeanVerb|code inline| in it.
128126
Here's when a \LeanVerb|code inline|
129127
occurs right before a line break.And then here's a paragraph break.
130128
\end{docstringBox}
131129

130+
131+
\mainmatter
132132
\end{document}

0 commit comments

Comments
 (0)