166 lines
3.9 KiB
TeX
166 lines
3.9 KiB
TeX
\documentclass[10pt]{book}
|
|
|
|
\usepackage{hyperref}
|
|
\usepackage[links]{agda}
|
|
\usepackage{fontspec}
|
|
\setmainfont{DejaVu Sans}
|
|
\setsansfont{DejaVu Sans}
|
|
\setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]}
|
|
\usepackage{soul}
|
|
\usepackage{tcolorbox}
|
|
\tcbuselibrary{skins,breakable}
|
|
\usepackage{fancyvrb}
|
|
\usepackage{xcolor}
|
|
\usepackage{tikz}
|
|
\usepackage{setspace}
|
|
\usepackage{geometry}
|
|
\geometry{
|
|
a4paper,
|
|
total={170mm,257mm},
|
|
left=20mm,
|
|
top=20mm,
|
|
}
|
|
|
|
|
|
% Wrap texttt lines
|
|
\sloppy
|
|
|
|
% Disable section numbering
|
|
\setcounter{secnumdepth}{0}
|
|
|
|
% Set the global text color:
|
|
\definecolor{textcolor}{HTML}{111111}
|
|
\color{textcolor}
|
|
|
|
% Change background color for inline code in markdown files.
|
|
% The following code does not work well for long text as the
|
|
% text will exceed the page boundary.
|
|
\definecolor{background-color}{HTML}{EEEEFF}
|
|
\let\oldtexttt\texttt%
|
|
\renewcommand{\texttt}[1]{\colorbox{background-color}{\oldtexttt{#1}}}
|
|
|
|
% Box with background colour similar to web version:
|
|
\newtcolorbox{agda}[1][]{
|
|
frame hidden,
|
|
colback=background-color,
|
|
spartan,
|
|
left=5pt,
|
|
boxrule=0pt,
|
|
breakable,
|
|
}
|
|
|
|
% Verbatim environment similarly indented to Agda code blocks.
|
|
\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt}%
|
|
|
|
% Adding backgrounds to verbatim environments.
|
|
\newenvironment{pre}{
|
|
\VerbatimEnvironment
|
|
\begin{agda}
|
|
\begin{verbatim}
|
|
}{\end{verbatim}
|
|
\end{agda}
|
|
}
|
|
|
|
% Use special font families without TeX ligatures for Agda code.
|
|
% Solution inspired by a comment by Enrico Gregorio:
|
|
% https://tex.stackexchange.com/a/103078
|
|
\newfontfamily{\AgdaSerifFont}{DejaVu-Serif}
|
|
\newfontfamily{\AgdaSansSerifFont}{DejaVu-Sans}
|
|
\newfontfamily{\AgdaTypewriterFont}{DejaVu-mononoki-Symbola-Droid}
|
|
\renewcommand{\AgdaFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
|
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
|
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
|
\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
|
\renewcommand{\AgdaBoundFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
|
|
|
\AgdaNoSpaceAroundCode{}
|
|
|
|
% Adjust spacing after toc numbering
|
|
\usepackage{tocloft}
|
|
\setlength\cftchapnumwidth{3em}
|
|
\cftsetpnumwidth{4em}
|
|
|
|
% Style links with colors instead of boxes:
|
|
% https://tex.stackexchange.com/q/823
|
|
\definecolor{linkcolor}{HTML}{2A7AE2}
|
|
\hypersetup{
|
|
colorlinks,
|
|
linkcolor={linkcolor},
|
|
citecolor={linkcolor},
|
|
urlcolor={linkcolor}
|
|
}
|
|
|
|
\begin{document}
|
|
|
|
% Adjust indentation of Agda code blocks
|
|
\setlength{\mathindent}{0pt}
|
|
\setlength{\parindent}{0em}
|
|
\setlength{\parskip}{1em}
|
|
|
|
% Provide \tightlist environment
|
|
% https://tex.stackexchange.com/q/257418
|
|
\providecommand{\tightlist}{%
|
|
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
|
|
|
|
% Based on \titleAM:
|
|
% https://ctan.org/pkg/titlepages
|
|
\begin{titlepage}
|
|
\newlength{\drop}%
|
|
\setlength{\drop}{0.12\textheight}%
|
|
\centering%
|
|
\vspace*{\drop}
|
|
\begingroup% Ancient Mariner, AW p. 151
|
|
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
|
|
{\Huge PROGRAMMING LANGUAGE}\\[\baselineskip]
|
|
{\Huge FOUNDATIONS}\\[\baselineskip]
|
|
{\Large IN}\\[\baselineskip]
|
|
{\Huge Agda}\\[\drop]
|
|
\vfill%
|
|
{\small\scshape 2021}\par%
|
|
\null\endgroup
|
|
\end{titlepage}
|
|
|
|
$for(parts)$
|
|
|
|
% Open front, main, and back matter sections:
|
|
$if(frontmatter)$
|
|
\frontmatter%
|
|
\setcounter{tocdepth}{0}
|
|
|
|
\tableofcontents%
|
|
\setcounter{tocdepth}{1}
|
|
$endif$
|
|
$if(mainmatter)$
|
|
\mainmatter%
|
|
$endif$
|
|
$if(backmatter)$
|
|
\appendix
|
|
\addcontentsline{toc}{part}{Appendices}
|
|
$endif$
|
|
|
|
% Only print title for main and back matter:
|
|
$if(frontmatter)$
|
|
% NOTE: Front matter titles are inserted via book/lua/single-file-headers.lua.
|
|
$else$
|
|
\part{$title$}
|
|
$endif$
|
|
|
|
% Include each section.
|
|
$for(sections)$
|
|
\hypertarget{$anchor$}{%
|
|
\chapter{$title$}\label{$anchor$}}
|
|
\input{$tex_path$}
|
|
$endfor$
|
|
|
|
% Close front, main, and back matter sections:
|
|
$if(frontmatter)$
|
|
$endif$
|
|
$if(mainmatter)$
|
|
\cleardoublepage%
|
|
\phantomsection%
|
|
$endif$
|
|
$if(backmatter)$
|
|
$endif$
|
|
$endfor$
|
|
|
|
\end{document}
|