Fixed PDF generation.

This commit is contained in:
Wen Kokke 2021-08-23 18:59:51 +01:00
parent d14b04ebf2
commit 587985aa9d
No known key found for this signature in database
GPG key ID: 7EB7DBBCEB539DB8

View file

@ -78,8 +78,6 @@
\AgdaNoSpaceAroundCode{} \AgdaNoSpaceAroundCode{}
\setlength{\parindent}{0em}
\setlength{\parskip}{1em}
% Adjust spacing after toc numbering % Adjust spacing after toc numbering
\usepackage{tocloft} \usepackage{tocloft}
@ -97,24 +95,27 @@
\begin{document} \begin{document}
% Adjust indentation of agda codeblocks % Adjust indentation of Agda code blocks
\setlength{\mathindent}{0pt} \setlength{\mathindent}{0pt}
\setlength{\parindent}{0em}
\setlength{\parskip}{1em}
% Provide \tightlist environment % Provide \tightlist environment
% https://tex.stackexchange.com/q/257418 % https://tex.stackexchange.com/q/257418
\providecommand{\tightlist}{% \providecommand{\tightlist}{%
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
% Based on \titleAM:
% https://ctan.org/pkg/titlepages % https://ctan.org/pkg/titlepages
% https://latex.org/forum/viewtopic.php?t=2843
\begin{titlepage} \begin{titlepage}
\newlength{\drop} \newlength{\drop}%
\setlength{\drop}{0.12\textheight}% \setlength{\drop}{0.12\textheight}%
\centering% \centering%
\vspace*{\drop}
\begingroup% Ancient Mariner, AW p. 151 \begingroup% Ancient Mariner, AW p. 151
\vspace*{\drop}%
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip] {\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
{\Huge PROGRAMMING LANGUAGE FOUNDATIONS}\\[\baselineskip] {\Huge PROGRAMMING LANGUAGE}\\[\baselineskip]
{\Huge FOUNDATIONS}\\[\baselineskip]
{\Large IN}\\[\baselineskip] {\Large IN}\\[\baselineskip]
{\Huge Agda}\\[\drop] {\Huge Agda}\\[\drop]
\vfill% \vfill%
@ -132,7 +133,8 @@
\input{plfa/frontmatter/preface} \input{plfa/frontmatter/preface}
\input{plfa/frontmatter/README} \input{plfa/frontmatter/README}
\mainmatter \mainmatter%
\part{Part 1: Logical Foundations} \part{Part 1: Logical Foundations}
\input{plfa/part1/Naturals} \input{plfa/part1/Naturals}
\input{plfa/part1/Induction} \input{plfa/part1/Induction}