From d14b04ebf25b4c37d3e5021344f5d7e9c2579cec Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 23 Aug 2021 18:34:35 +0100 Subject: [PATCH] Fixed PDF generation. --- Makefile | 140 +++- pdf/Makefile | 128 ---- pdf/README.md | 20 - pdf/agda.sty | 708 ------------------ pdf/codeblocks-readme.lua | 7 - pdf/codeblocks.lua | 11 - pdf/handle-badges.lua | 5 - pdf/lua/remove-badges.lua | 12 + pdf/{ => lua}/rewrite-links.lua | 0 .../single-file-headers-ids.lua} | 31 +- pdf/lua/typeset-codeblocks.lua | 49 ++ pdf/plfa-sample.tex | 171 ----- pdf/plfa.agda-lib | 3 - pdf/plfa.tex | 200 ++--- .../acknowledgements.latex} | 0 .../chapter.latex} | 0 src/plfa/part3/Denotational.lagda.md | 2 +- 17 files changed, 315 insertions(+), 1172 deletions(-) delete mode 100644 pdf/Makefile delete mode 100644 pdf/README.md delete mode 100644 pdf/agda.sty delete mode 100644 pdf/codeblocks-readme.lua delete mode 100644 pdf/codeblocks.lua delete mode 100644 pdf/handle-badges.lua create mode 100644 pdf/lua/remove-badges.lua rename pdf/{ => lua}/rewrite-links.lua (100%) rename pdf/{header-id.lua => lua/single-file-headers-ids.lua} (64%) create mode 100644 pdf/lua/typeset-codeblocks.lua delete mode 100644 pdf/plfa-sample.tex delete mode 100644 pdf/plfa.agda-lib rename pdf/{lagdamd2tex_acknowledgement.latex => templates/acknowledgements.latex} (100%) rename pdf/{lagdamd2tex_chapter.latex => templates/chapter.latex} (100%) diff --git a/Makefile b/Makefile index 7d39b90e..7a40b317 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,13 @@ SITE_DIR := _site CACHE_DIR := _cache TMP_DIR := $(CACHE_DIR)/tmp +AGDA := stack exec agda -- \ + --no-libraries \ + --include-path=standard-library/src +PANDOC := stack exec pandoc -- \ + --indented-code-classes=default + --top-level-division=chapter + ################################################################################# # Setup Git Hooks @@ -29,6 +36,7 @@ standard-library/ChangeLog.md: git submodule init git submodule update --recursive + ################################################################################# # Test generated site with HTMLProofer ################################################################################# @@ -48,6 +56,7 @@ test: setup-install-htmlproofer build --check-opengraph \ . + ################################################################################# # Test generated EPUB with EPUBCheck ################################################################################# @@ -152,6 +161,120 @@ endif endif +################################################################################# +# Build PDF +################################################################################# + +PDF_DIR := pdf +PDF_TEMPLATE_DIR := $(PDF_DIR)/templates +PDF_LUA_DIR := $(PDF_DIR)/lua +MD_DIR := src +LAGDA_TEX_DIR := $(TMP_DIR)/lagda_tex +TEX_DIR := $(TMP_DIR)/tex + +# Convert MD_DIR/%.lagda.md to LAGDA_TEX_DIR/%.lagda.tex +define LAGDA_TEX_PATH +$(patsubst $(MD_DIR)/%.lagda.md,$(LAGDA_TEX_DIR)/%.lagda.tex,$(1)) +endef + +# Convert MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex or TEX_DIR/%.tex +define TEX_PATH +$(patsubst $(PDF_DIR)/%,$(TEX_DIR)/%,\ + $(patsubst README.md,$(TEX_DIR)/plfa/frontmatter/README.tex,\ + $(patsubst $(MD_DIR)/%.md,$(TEX_DIR)/%.tex,\ + $(patsubst $(MD_DIR)/%.lagda.md,$(TEX_DIR)/%.tex,$(1))))) +endef + +# List source and intermediate files +PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua) +PDF_STATIC_FILES := $(wildcard pdf/*.*) +MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md) +LAGDA_MD_FILES := $(filter %.lagda.md,$(MD_FILES)) +LAGDA_TEX_FILES := $(call LAGDA_TEX_PATH,$(LAGDA_MD_FILES)) +TEX_FILES := $(call TEX_PATH,$(MD_FILES) $(PDF_STATIC_FILES)) + +# Compile PLFA to a PDF +.PHONY: pdf +pdf: $(SITE_DIR)/plfa.pdf + +$(SITE_DIR)/plfa.pdf: $(TEX_FILES) + @cd $(TEX_DIR) && latexmk -pdf -lualatex -use-make -halt-on-error plfa.tex + @cp $(TEX_DIR)/plfa.pdf $(SITE_DIR)/plfa.pdf + + +# Copy static files needed by PDF compilation +define MK_COPYSTATIC_RULE +src := $(1) +dst := $(2) +$$(dst): $$(src) + @echo "Copy $$< to $$@" + @cp $$< $$@ +endef + +# Compile Markdown files to LaTeX +define MK_MD2TEX_RULE +src := $(1) +dst := $(2) +tpl := $(3) +$$(dst): export UNCHECKED_FILES = README.md +$$(dst): $$(src) $$(tpl) $(PDF_LUA_SCRIPTS) | setup-install-pandoc + @echo "Compile $$< to $$@" + @mkdir -p '$$(@D)' + @$(PANDOC) \ + --lua-filter=$(PDF_LUA_DIR)/remove-badges.lua \ + --lua-filter=$(PDF_LUA_DIR)/typeset-codeblocks.lua \ + --lua-filter=$(PDF_LUA_DIR)/rewrite-links.lua \ + --lua-filter=$(PDF_LUA_DIR)/single-file-headers-ids.lua \ + --template=$$(tpl) \ + $$< -o $$@ +endef + +# Compile Literate Agda files to LaTeX +define MK_LAGDA_MD2TEX_RULE +src := $(1) +dst := $(2) +$$(dst): $$(src) $(LAGDA_TEX_FILES) | setup-install-agda + @$(AGDA) --include-path=$(LAGDA_TEX_DIR) --latex --latex-dir=$(TEX_DIR) $$< +endef + + +# Copy static files (from PDF_DIR/% to TEX_DIR/%) +$(foreach static_file,\ + $(PDF_STATIC_FILES),\ + $(eval $(call MK_COPYSTATIC_RULE,\ + $(static_file),\ + $(call TEX_PATH,$(static_file))))) + +# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex) +$(foreach md_file,\ + $(filter-out %acknowledgements.md %.lagda.md,$(MD_FILES)),\ + $(eval $(call MK_MD2TEX_RULE,\ + $(md_file),\ + $(call TEX_PATH,$(md_file)),\ + $(PDF_TEMPLATE_DIR)/chapter.latex))) + +# Compile .lagda.md files (from MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex) +$(foreach lagda_md_file,\ + $(LAGDA_MD_FILES),\ + $(eval $(call MK_MD2TEX_RULE,\ + $(lagda_md_file),\ + $(call LAGDA_TEX_PATH,$(lagda_md_file)),\ + $(PDF_TEMPLATE_DIR)/chapter.latex))) + +# Compile acknowledgements (from SITE_DIR/acknowledgements.md to TEX_DIR/acknowledgements.tex) +$(eval $(call MK_MD2TEX_RULE,\ + $(SITE_DIR)/acknowledgements.md,\ + $(TEX_DIR)/plfa/backmatter/acknowledgements.tex,\ + $(PDF_TEMPLATE_DIR)/acknowledgements.latex)) + +# Compile .lagda.tex files (from LAGDA_TEX_DIR/%.lagda.tex to TEX_DIR/%.tex) +$(foreach lagda_md_file,\ + $(LAGDA_MD_FILES),\ + $(eval $(call MK_LAGDA_MD2TEX_RULE,\ + $(call LAGDA_TEX_PATH,$(lagda_md_file)),\ + $(call TEX_PATH,$(lagda_md_file))))) + + ################################################################################# # Setup dependencies ################################################################################# @@ -218,6 +341,19 @@ ifeq (,$(wildcard $(shell which bundle))) gem install bundle endif +.PHONY: setup-install-agda +setup-install-agda: setup-check-stack +ifeq (,$(wildcard $(shell stack exec which -- agda))) + @echo "Installing Agda" + stack build --only-dependencies +endif + +.PHONY: setup-install-pandoc +setup-install-pandoc: setup-check-stack +ifeq (,$(wildcard $(shell stack exec which -- pandoc))) + @echo "Installing Pandoc" + stack build --only-dependencies +endif ################################################################################# # Build legacy versions of website using Jekyll @@ -269,7 +405,3 @@ versions/$$(out): $$(tmp_dir) endef $(foreach legacy_version,$(LEGACY_VERSIONS),$(eval $(call build_legacy_version,$(legacy_version)))) - -.PHONY: pdf -pdf: - make -C pdf \ No newline at end of file diff --git a/pdf/Makefile b/pdf/Makefile deleted file mode 100644 index af841b10..00000000 --- a/pdf/Makefile +++ /dev/null @@ -1,128 +0,0 @@ -# To use the makefile, specify the path to source files under SRC -# and the path to pandoc-filters under FILTERS - - -.PHONY: all clean - -SRC := ../src -SITE := ../_site -front_and_back := latex/plfa/frontmatter/dedication.tex latex/plfa/frontmatter/README.tex\ - latex/plfa/frontmatter/preface.tex latex/plfa/backmatter/acknowledgements.tex -lagda_md_files := $(shell find $(SRC) -name '*.lagda.md') -transpiled_files := $(patsubst $(SRC)/%.md,lagda_tex/%.tex,$(lagda_md_files)) -latex_files := $(patsubst $(SRC)/%.lagda.md,latex/%.tex,$(lagda_md_files)) -pdfs := $(patsubst $(SRC)/%.lagda.md,pdf/%.pdf,$(lagda_md_files)) - -# for make to clean file in subdirectories -# https://stackoverflow.com/questions/4210042/exclude-directory-from-find-command -SUBDIR_ROOTS := tex latex -DIRS := . $(shell find $(SUBDIR_ROOTS) -type d) -GARBAGE_TYPES := *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls -GARBAGE_TYPED_FOLDERS := $(foreach DIR, $(DIRS), $(addprefix $(DIR)/,$(GARBAGE_TYPES))) - -all: all_tex plfa.pdf - -# A pdf for the whole book -plfa.pdf: $(latex_files) plfa.tex $(front_and_back) - latexmk -pdf -lualatex -use-make plfa.tex - -plfa-sample.pdf: $(latex_files) plfa-sample.tex $(front_and_back) - latexmk -pdf -lualatex -use-make plfa-sample.tex - -all_tex: $(transpiled_files) -all_latex: $(latex_files) -all_pdfs : $(pdfs) - - - -# General Rules - -# from https://stackoverflow.com/questions/48267813/makefile-compile-objects-to-different-directory-and-build-from-there -# make a different directory for lagda.tex -# --shift-heading-level-by=-1 is a good choice -# when converting HTML or Markdown documents that use an initial level-1 heading -# also can try treat first heading as chapter -# by using --top-level-division=chapter -# for the document title and level-2+ headings for sections. -lagda_tex/%.lagda.tex : $(SRC)/%.lagda.md \ - codeblocks.lua rewrite-links.lua header-id.lua \ - lagdamd2tex_chapter.latex - @echo "Transpiling $< into $@" - @mkdir -p '$(@D)' - pandoc $< --indented-code-classes=default \ - --lua-filter ./codeblocks.lua \ - --lua-filter ./rewrite-links.lua \ - --lua-filter ./header-id.lua \ - --top-level-division=chapter \ - -o $@ \ - --template=lagdamd2tex_chapter.latex - -# run agda under same directory with lagda.tex -latex/%.tex : lagda_tex/%.lagda.tex - cd lagda_tex; agda --latex-dir=../latex \ - --latex $(subst lagda_tex/,,$<) - - -pdf/%.pdf: latex/%.tex - @echo $< - latexmk -pdf -output-directory="pdf" -lualatex -use-make $< - -# Specific rules for .md files, could be optimized! -# for general frontmatter -latex/plfa/frontmatter/%.tex : $(SRC)/plfa/frontmatter/%.md codeblocks-readme.lua - @echo "Transpiling $< into $@" - @mkdir -p '$(@D)' - pandoc $< --indented-code-classes=default \ - --lua-filter ./codeblocks-readme.lua \ - --lua-filter ./header-id.lua \ - --top-level-division=chapter \ - -o $@ \ - --template=lagdamd2tex_chapter.latex -# for readme -latex/plfa/frontmatter/README.tex : ../README.md codeblocks-readme.lua header-id.lua handle-badges.lua \ - lagdamd2tex_chapter.latex - @echo "Transpiling $< into $@" - @mkdir -p '$(@D)' - pandoc $< --indented-code-classes=default \ - --lua-filter ./codeblocks-readme.lua \ - --lua-filter ./header-id.lua \ - --lua-filter ./handle-badges.lua \ - --top-level-division=chapter \ - -o $@ \ - --template=lagdamd2tex_chapter.latex - -# process for acknowledgements -# generate in _site/acknowledgements.md -../_site/acknowledgements.md : $(SRC)/plfa/backmatter/acknowledgements.md - cd ..; stack build && stack exec site build - -# transpile once to html to unify the lists -acknowledgements.html : $(SITE)/acknowledgements.md - pandoc -o $@ $< - -# compile the above version to latex -latex/plfa/backmatter/acknowledgements.tex : acknowledgements.html lagdamd2tex_acknowledgement.latex - @echo "Transpiling $< into $@" - @mkdir -p '$(@D)' - pandoc $< --indented-code-classes=default \ - --top-level-division=chapter \ - -o $@ \ - --template=lagdamd2tex_acknowledgement.latex - - -# general backmatter -latex/plfa/backmatter/%.tex : $(SRC)/plfa/backmatter/%.md codeblocks-readme.lua lagdamd2tex_chapter.latex - @echo "Transpiling $< into $@" - @mkdir -p '$(@D)' - pandoc $< --indented-code-classes=default \ - --lua-filter ./codeblocks-readme.lua \ - --lua-filter ./header-id.lua \ - --top-level-division=chapter \ - -o $@ \ - --template=lagdamd2tex_chapter.latex - - - -clean: - $(RM) -rf $(GARBAGE_TYPED_FOLDERS) - diff --git a/pdf/README.md b/pdf/README.md deleted file mode 100644 index ce9d3dcb..00000000 --- a/pdf/README.md +++ /dev/null @@ -1,20 +0,0 @@ -This directory contains the files needed for building a pdf version of the book. Notice the structure is important here: the makefile and latex commands are written based on relative paths. - -Dependencies (relative to the root): -- all things under `pdf/` except `lagda_tex/` and `latex/`. The latter two are generated by the makefile and uploaded for compiling speed. -- agda source files under `src/` -- `_site/acknowledgements.md` generated when building the site -- `README.md` -- the font `DejaVu mononoki Symbola Droid` installed globally. (Could change to local?) - -First, run `stack build && stack exec site rebuild` from the parent directory to generate acknowledgements.md under `_site`, which is needed by the pdf (Only need to do this once). - -Then, running `make pdf` from the parent directory should be sufficient to compile the book. The book will be generated in this folder as `plfa.pdf`. - -Alternatively, makefile in this directory provide these options: - -```make -all # Build plfa.pdf (can also run from the parent as "make pdf") -plfa-sample.pdf # Build a shrinked version of the book for testing -all_tex # generate all tex version of lagda files under tex/ -``` diff --git a/pdf/agda.sty b/pdf/agda.sty deleted file mode 100644 index c14cda7a..00000000 --- a/pdf/agda.sty +++ /dev/null @@ -1,708 +0,0 @@ -% ---------------------------------------------------------------------- -% Some useful commands when doing highlighting of Agda code in LaTeX. -% ---------------------------------------------------------------------- - -\ProvidesPackage{agda} - -\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, - calc, environ, xparse, xkeyval} - -% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation -\newif\ifxetexorluatex -\ifxetex - \xetexorluatextrue -\else - \ifluatex - \xetexorluatextrue - \else - \xetexorluatexfalse - \fi -\fi - -% ---------------------------------------------------------------------- -% Options - -\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}} -\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}} - -\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse -\DeclareOption{references}{ - \@AgdaEnableReferencestrue -} - -\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse -\DeclareOption{links}{ - \@AgdaEnableLinkstrue -} - -\ProcessOptions\relax - -% ---------------------------------------------------------------------- -% Font setup - -\tracinglostchars=2 % If the font is missing some symbol, then say - % so in the compilation output. - -% ---------------------------------------------------------------------- -% Colour schemes. - -\providecommand{\AgdaColourScheme}{standard} - -% ---------------------------------------------------------------------- -% References to code (needs additional post-processing of tex files to -% work, see wiki for details). - -\if@AgdaEnableReferences - \RequirePackage{catchfilebetweentags, xstring} - \newcommand{\AgdaRef}[2][]{% - \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]% - \ifthenelse{\isempty{#1}}% - {\ExecuteMetaData{AgdaTag-\tmp}}% - {\ExecuteMetaData{#1}{AgdaTag-\tmp}} - } -\fi - -\providecommand{\AgdaRef}[2][]{#2} - -% ---------------------------------------------------------------------- -% Links (only done if the option is passed and the user has loaded the -% hyperref package). - -\if@AgdaEnableLinks - \@ifpackageloaded{hyperref}{ - - % List that holds added targets. - \newcommand{\AgdaList}[0]{} - - \newtoggle{AgdaIsElem} - \newcounter{AgdaIndex} - \newcommand{\AgdaLookup}[3]{% - \togglefalse{AgdaIsElem}% - \setcounter{AgdaIndex}{0}% - \renewcommand*{\do}[1]{% - \ifstrequal{#1}{##1}% - {\toggletrue{AgdaIsElem}\listbreak}% - {\stepcounter{AgdaIndex}}}% - \dolistloop{\AgdaList}% - \iftoggle{AgdaIsElem}{#2}{#3}% - } - - \newcommand*{\AgdaTargetHelper}[1]{% - \AgdaLookup{#1}% - {\PackageError{agda}{``#1'' used as target more than once}% - {Overloaded identifiers and links do not% - work well, consider using unique% - \MessageBreak identifiers instead.}% - }% - {\listadd{\AgdaList}{#1}% - \hypertarget{Agda\theAgdaIndex}{}% - }% - } - - \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}} - - \newcommand{\AgdaLink}[1]{% - \AgdaLookup{#1}% - {\hyperlink{Agda\theAgdaIndex}{#1}}% - {#1}% - } - }{\PackageError{agda}{Load the hyperref package before the agda package}{}} -\fi - -\providecommand{\AgdaTarget}[1]{} -\providecommand{\AgdaLink}[1]{#1} - -% ---------------------------------------------------------------------- -% Font styles. - -\newcommand{\AgdaFontStyle}[1]{\texttt{#1}} -\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ - \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}} -}{ - \newcommand{\AgdaKeywordFontStyle}[1]{\texttt{#1}} -} -\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}} -\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}} -\newcommand{\AgdaBoundFontStyle}[1]{\texttt{#1}} - -% ---------------------------------------------------------------------- -% Colours. - -% ---------------------------------- -% The black and white colour scheme. -\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ - - % Aspect colours. - \definecolor{AgdaComment} {HTML}{000000} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{000000} - \definecolor{AgdaString} {HTML}{000000} - \definecolor{AgdaNumber} {HTML}{000000} - \definecolor{AgdaSymbol} {HTML}{000000} - \definecolor{AgdaPrimitiveType}{HTML}{000000} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{000000} - \definecolor{AgdaGeneralizable} {HTML}{000000} - \definecolor{AgdaInductiveConstructor} {HTML}{000000} - \definecolor{AgdaCoinductiveConstructor}{HTML}{000000} - \definecolor{AgdaDatatype} {HTML}{000000} - \definecolor{AgdaField} {HTML}{000000} - \definecolor{AgdaFunction} {HTML}{000000} - \definecolor{AgdaMacro} {HTML}{000000} - \definecolor{AgdaModule} {HTML}{000000} - \definecolor{AgdaPostulate} {HTML}{000000} - \definecolor{AgdaPrimitive} {HTML}{000000} - \definecolor{AgdaRecord} {HTML}{000000} - \definecolor{AgdaArgument} {HTML}{000000} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3} - \definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3} - \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE} - \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3} - \definecolor{AgdaError} {HTML}{696969} - - % Misc. - \definecolor{AgdaHole} {HTML}{BEBEBE} - -% ---------------------------------- -% Conor McBride's colour scheme. -}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{ - - % Aspect colours. - \definecolor{AgdaComment} {HTML}{B22222} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{000000} - \definecolor{AgdaString} {HTML}{000000} - \definecolor{AgdaNumber} {HTML}{000000} - \definecolor{AgdaSymbol} {HTML}{000000} - \definecolor{AgdaPrimitiveType}{HTML}{0000CD} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{A020F0} - \definecolor{AgdaGeneralizable} {HTML}{A020F0} - \definecolor{AgdaInductiveConstructor} {HTML}{8B0000} - \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000} - \definecolor{AgdaDatatype} {HTML}{0000CD} - \definecolor{AgdaField} {HTML}{8B0000} - \definecolor{AgdaFunction} {HTML}{006400} - \definecolor{AgdaMacro} {HTML}{006400} - \definecolor{AgdaModule} {HTML}{006400} - \definecolor{AgdaPostulate} {HTML}{006400} - \definecolor{AgdaPrimitive} {HTML}{006400} - \definecolor{AgdaRecord} {HTML}{0000CD} - \definecolor{AgdaArgument} {HTML}{404040} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{FFD700} - \definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700} - \definecolor{AgdaTerminationProblem}{HTML}{FF0000} - \definecolor{AgdaIncompletePattern} {HTML}{A020F0} - \definecolor{AgdaError} {HTML}{F4A460} - - % Misc. - \definecolor{AgdaHole} {HTML}{9DFF9D} - -% ---------------------------------- -% The standard colour scheme. -}{ - % Aspect colours. - \definecolor{AgdaComment} {HTML}{B22222} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{CD6600} - \definecolor{AgdaString} {HTML}{B22222} - \definecolor{AgdaNumber} {HTML}{A020F0} - \definecolor{AgdaSymbol} {HTML}{404040} - \definecolor{AgdaPrimitiveType}{HTML}{0000CD} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{000000} - \definecolor{AgdaGeneralizable} {HTML}{000000} - \definecolor{AgdaInductiveConstructor} {HTML}{008B00} - \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500} - \definecolor{AgdaDatatype} {HTML}{0000CD} - \definecolor{AgdaField} {HTML}{EE1289} - \definecolor{AgdaFunction} {HTML}{0000CD} - \definecolor{AgdaMacro} {HTML}{458B74} - \definecolor{AgdaModule} {HTML}{A020F0} - \definecolor{AgdaPostulate} {HTML}{0000CD} - \definecolor{AgdaPrimitive} {HTML}{0000CD} - \definecolor{AgdaRecord} {HTML}{0000CD} - \definecolor{AgdaArgument} {HTML}{404040} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00} - \definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00} - \definecolor{AgdaTerminationProblem}{HTML}{FFA07A} - \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3} - \definecolor{AgdaError} {HTML}{FF0000} - - % Misc. - \definecolor{AgdaHole} {HTML}{9DFF9D} -}} - -% ---------------------------------------------------------------------- -% Commands. - -\newcommand{\AgdaNoSpaceMath}[1] - {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup} - -% Aspect commands. -\newcommand{\AgdaComment} [1] - {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}} -\newcommand{\AgdaPragma} [1] - {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaPragma}{#1}}}} -\newcommand{\AgdaKeyword} [1] - {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}} -\newcommand{\AgdaString} [1] - {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}} -\newcommand{\AgdaNumber} [1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}} -\newcommand{\AgdaSymbol} [1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}} -\newcommand{\AgdaPrimitiveType}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}} -% Note that, in code generated by the LaTeX backend, \AgdaOperator is -% always applied to a NameKind command. -\newcommand{\AgdaOperator} [1]{#1} - -% NameKind commands. - -% The user can control the typesetting of (certain) individual tokens -% by redefining the following command. The first argument is the token -% and the second argument the thing to be typeset (sometimes just the -% token, sometimes \AgdaLink{}). Example: -% -% \usepackage{ifthen} -% -% % Insert extra space before some tokens. -% \DeclareRobustCommand{\AgdaFormat}[2]{% -% \ifthenelse{ -% \equal{#1}{≡⟨} \OR -% \equal{#1}{≡⟨⟩} \OR -% \equal{#1}{∎} -% }{\ }{}#2} -% -% Note the use of \DeclareRobustCommand. - -\newcommand{\AgdaFormat}[2]{#2} - -\newcommand{\AgdaBound}[1] - {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaGeneralizable}[1] - {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaGeneralizable}{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaInductiveConstructor}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaCoinductiveConstructor}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaDatatype}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaField}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaFunction}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaMacro}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaModule}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaPostulate}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaPrimitive}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaRecord}[1] - {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaArgument}[1] - {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}} - -% Other aspect commands. -\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}} -\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}} -\newcommand{\AgdaUnsolvedMeta} [1] - {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}} -\newcommand{\AgdaUnsolvedConstraint}[1] - {\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}} -\newcommand{\AgdaTerminationProblem}[1] - {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}} -\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}} -\newcommand{\AgdaError} [1] - {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}} -\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this - -% Used to hide code from LaTeX. -% -% Note that this macro has been deprecated in favour of giving the -% hide argument to the code environment. -\long\def\AgdaHide#1{\ignorespaces} - -% Misc. -\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}} - -% ---------------------------------------------------------------------- -% The code environment. - -\newcommand{\AgdaCodeStyle}{} -% \newcommand{\AgdaCodeStyle}{\tiny} - -\ifdefined\mathindent - {} -\else - \newdimen\mathindent\mathindent\leftmargini -\fi - -% Adds the given amount of vertical space and starts a new line. -% -% The implementation comes from lhs2TeX's polycode.fmt, written by -% Andres Löh. -\newcommand{\Agda@NewlineWithVerticalSpace}[1]{% - {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}} - -% Should there be space around code? -\newboolean{Agda@SpaceAroundCode} - -% Use this command to avoid extra space around code blocks. -\newcommand{\AgdaNoSpaceAroundCode}{% - \setboolean{Agda@SpaceAroundCode}{false}} - -% Use this command to include extra space around code blocks. -\newcommand{\AgdaSpaceAroundCode}{% - \setboolean{Agda@SpaceAroundCode}{true}} - -% By default space is inserted around code blocks. -\AgdaSpaceAroundCode{} - -% Sometimes one might want to break up a code block into multiple -% pieces, but keep code in different blocks aligned with respect to -% each other. Then one can use the AgdaAlign environment. Example -% usage: -% -% \begin{AgdaAlign} -% \begin{code} -% code -% code (more code) -% \end{code} -% Explanation... -% \begin{code} -% aligned with "code" -% code (aligned with (more code)) -% \end{code} -% \end{AgdaAlign} -% -% Note that AgdaAlign environments should not be nested. -% -% Sometimes one might also want to hide code in the middle of a code -% block. This can be accomplished in the following way: -% -% \begin{AgdaAlign} -% \begin{code} -% visible -% \end{code} -% \begin{code}[hide] -% hidden -% \end{code} -% \begin{code} -% visible -% \end{code} -% \end{AgdaAlign} -% -% However, the result may be ugly: extra space is perhaps inserted -% around the code blocks. -% -% The AgdaSuppressSpace environment ensures that extra space is only -% inserted before the first code block, and after the last one (but -% not if \AgdaNoSpaceAroundCode{} is used). Example usage: -% -% \begin{AgdaAlign} -% \begin{code} -% code -% more code -% \end{code} -% Explanation... -% \begin{AgdaSuppressSpace} -% \begin{code} -% aligned with "code" -% aligned with "more code" -% \end{code} -% \begin{code}[hide] -% hidden code -% \end{code} -% \begin{code} -% also aligned with "more code" -% \end{code} -% \end{AgdaSuppressSpace} -% \end{AgdaAlign} -% -% Note that AgdaSuppressSpace environments should not be nested. -% -% There is also a combined environment, AgdaMultiCode, that combines -% the effects of AgdaAlign and AgdaSuppressSpace. - -% The number of the current/next code block (excluding hidden ones). -\newcounter{Agda@Current} -\setcounter{Agda@Current}{0} - -% The number of the previous code block (excluding hidden ones), used -% locally in \Agda@SuppressEnd. -\newcounter{Agda@Previous} - -% Is AgdaAlign active? -\newboolean{Agda@Align} -\setboolean{Agda@Align}{false} - -% The number of the first code block (if any) in a given AgdaAlign -% environment. -\newcounter{Agda@AlignStart} - -\newcommand{\Agda@AlignStart}{% - \ifthenelse{\boolean{Agda@Align}}{% - \PackageError{agda}{Nested AgdaAlign environments}{% - AgdaAlign and AgdaMultiCode environments must not be - nested.}}{% - \setboolean{Agda@Align}{true}% - \setcounter{Agda@AlignStart}{\value{Agda@Current}}}} - -\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}} - -\newenvironment{AgdaAlign}{% - \Agda@AlignStart{}}{% - \Agda@AlignEnd{}% - \ignorespacesafterend} - -% Is AgdaSuppressSpace active? -\newboolean{Agda@Suppress} -\setboolean{Agda@Suppress}{false} - -% The number of the first code block (if any) in a given -% AgdaSuppressSpace environment. -\newcounter{Agda@SuppressStart} - -% Does a "do not suppress space after" label exist for the current -% code block? (This boolean is used locally in the code environment's -% implementation.) -\newboolean{Agda@DoNotSuppressSpaceAfter} - -\newcommand{\Agda@SuppressStart}{% - \ifthenelse{\boolean{Agda@Suppress}}{% - \PackageError{agda}{Nested AgdaSuppressSpace environments}{% - AgdaSuppressSpace and AgdaMultiCode environments must not be - nested.}}{% - \setboolean{Agda@Suppress}{true}% - \setcounter{Agda@SuppressStart}{\value{Agda@Current}}}} - -% Marks the given code block as one that space should not be -% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are -% both active). -\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{% - % The use of labels is intended to ensure that LaTeX will provide a - % warning if the document needs to be recompiled. - \label{Agda@DoNotSuppressSpaceAfter@#1}} - -\newcommand{\Agda@SuppressEnd}{% - \ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{% - % Mark the previous code block in the .aux file. - \setcounter{Agda@Previous}{\theAgda@Current-1}% - \immediate\write\@auxout{% - \noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}% - \setboolean{Agda@Suppress}{false}} - -\newenvironment{AgdaSuppressSpace}{% - \Agda@SuppressStart{}}{% - \Agda@SuppressEnd{}% - \ignorespacesafterend} - -\newenvironment{AgdaMultiCode}{% - \Agda@AlignStart{}% - \Agda@SuppressStart{}}{% - \Agda@SuppressEnd{}% - \Agda@AlignEnd{}% - \ignorespacesafterend} - -% Vertical space used for empty lines. By default \abovedisplayskip. -\newlength{\AgdaEmptySkip} -\setlength{\AgdaEmptySkip}{\abovedisplayskip} - -% Extra space to be inserted for empty lines (the difference between -% \AgdaEmptySkip and \baselineskip). Used internally. -\newlength{\AgdaEmptyExtraSkip} - -% Counter used for code numbers. -\newcounter{AgdaCodeNumber} -% Formats a code number. -\newcommand{\AgdaFormatCodeNumber}[1]{(#1)} - -% A boolean used to handle the option number. -\newboolean{Agda@Number} -\setboolean{Agda@Number}{false} - -% A boolean used to handle the option inline*. (For some reason the -% approach used for hide and inline does not work for inline*.) -\newboolean{Agda@InlineStar} -\setboolean{Agda@InlineStar}{false} - -% Keys used by the code environment. -\define@boolkey[Agda]{code}{hide}[true]{} -\define@boolkey[Agda]{code}{inline}[true]{} -\define@boolkey[Agda]{code}{inline*}[true]{% - \setboolean{Agda@InlineStar}{true}} -\define@key[Agda]{code}{number}[]{% - \ifthenelse{\boolean{Agda@Number}}{}{% - \setboolean{Agda@Number}{true}% - % Increase the counter if this has not already been done. - \refstepcounter{AgdaCodeNumber}}% - % If the label is non-empty, set it. Note that it is possible to - % give several labels for a single code listing. - \ifthenelse{\equal{#1}{}}{}{\label{#1}}} - -% The code environment. -% -% Options: -% -% * hide: The code is hidden. Other options are ignored. -% -% * number: Give the code an equation number. -% -% * number=l: Give the code an equation number and the label l. It is -% possible to use this option several times with different labels. -% -% * inline/inline*: The code is inlined. In this case most of the -% discussion above does not apply, alignment is not respected, and so -% on. It is recommended to only use this option for a single line of -% code, and to not use two consecutive spaces in this piece of code. -% -% Note that this environment ignores spaces after its end. If a space -% (\AgdaSpace{}) should be inserted after the inline code, use -% inline*, otherwise use inline. -% -% When this option is used number is ignored. -% -% The implementation is based on plainhscode in lhs2TeX's -% polycode.fmt, written by Andres Löh. -\NewEnviron{code}[1][]{% - % Process the options. Complain about unknown options. - \setkeys[Agda]{code}[number]{#1}% - \ifAgda@code@hide% - % Hide the code. - \else% - \ifAgda@code@inline% - % Inline code. - % - % Make the polytable primitives emitted by the LaTeX backend - % do nothing. - \DeclareDocumentCommand{\>}{O{}O{}}{}% - \DeclareDocumentCommand{\<}{O{}}{}% - \AgdaCodeStyle\BODY% - \else% - \ifthenelse{\boolean{Agda@InlineStar}}{% - % Inline code with space at the end. - % - \DeclareDocumentCommand{\>}{O{}O{}}{}% - \DeclareDocumentCommand{\<}{O{}}{}% - \AgdaCodeStyle\BODY\AgdaSpace{}}{% - % - % Displayed code. - % - % Conditionally emit space before the code block. Unconditionally - % switch to a new line. - \ifthenelse{\boolean{Agda@SpaceAroundCode} \and% - \(\not \boolean{Agda@Suppress} \or% - \value{Agda@SuppressStart} = \value{Agda@Current}\)}{% - \Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{% - \Agda@NewlineWithVerticalSpace{0pt}}% - % - % Check if numbers have been requested. If they have, then a side - % effect of this call is that Agda@Number is set to true, the code - % number counter is increased, and the label (if any) is set. - \setkeys[Agda]{code}[hide,inline,inline*]{#1}% - \ifthenelse{\boolean{Agda@Number}}{% - % Equation numbers have been requested. Use a minipage, so that - % there is room for the code number to the right, and the code - % number becomes centered vertically. - \begin{minipage}{% - \linewidth-% - \widthof{% - \AgdaSpace{}% - \AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}% - % - % Indent the entire code block. - \advance\leftskip\mathindent% - % - % The code's style can be customised. - \AgdaCodeStyle% - % - % Used to control the height of empty lines. - \setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}% - % - % The environment used to handle indentation (of individual lines) - % and alignment. - \begin{pboxed}% - % - % Conditionally preserve alignment between code blocks. - \ifthenelse{\boolean{Agda@Align}}{% - \ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{% - \savecolumns}{% - \restorecolumns}}{}% - % - % The code. - \BODY% - \end{pboxed}% - % - \ifthenelse{\boolean{Agda@Number}}{% - % Equation numbers have been requested. - \end{minipage}% - % Insert the code number to the right. - \hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}% - % - % Does the label Agda@DoNotSuppressAfter@ exist? - \ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{% - \setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{% - \setboolean{Agda@DoNotSuppressSpaceAfter}{false}}% - % - % Conditionally emit space after the code block. Unconditionally - % switch to a new line. - \ifthenelse{\boolean{Agda@SpaceAroundCode} \and% - \(\not \boolean{Agda@Suppress} \or% - \boolean{Agda@DoNotSuppressSpaceAfter}\)}{% - \Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{% - \Agda@NewlineWithVerticalSpace{0pt}}% - % - % Step the code block counter, but only for non-hidden code. - \stepcounter{Agda@Current}}% - \fi% - \fi% - % Reset Agda@Number and Agda@InlineStar. - \setboolean{Agda@Number}{false}% - \setboolean{Agda@InlineStar}{false}} - -% Space inserted after tokens. -\newcommand{\AgdaSpace}{ } - -% Space inserted to indent something. -\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$} - -% Default column for polytable. -\defaultcolumn{@{}l@{\AgdaSpace{}}} - -% \AgdaIndent expects a non-negative integer as its only argument. -% This integer should be the distance, in code blocks, to the thing -% relative to which the text is indented. -% -% The default implementation only indents if the thing that the text -% is indented relative to exists in the same code block or is wrapped -% in the same AgdaAlign or AgdaMultiCode environment. -\newcommand{\AgdaIndent}[1]{% - \ifthenelse{#1 = 0 - \or - \( \boolean{Agda@Align} - \and - \cnttest{\value{Agda@Current} - #1}{>=}{ - \value{Agda@AlignStart}} - \)}{\AgdaIndentSpace{}}{}} - -% Underscores are typeset using \AgdaUnderscore{}. -\newcommand{\AgdaUnderscore}{\_} - -\endinput diff --git a/pdf/codeblocks-readme.lua b/pdf/codeblocks-readme.lua deleted file mode 100644 index a8616e1c..00000000 --- a/pdf/codeblocks-readme.lua +++ /dev/null @@ -1,7 +0,0 @@ --- tested on pandoc 2.2.3.2 --- from agda doc: --- Code blocks start with ``` or ```agda on its own line, and end with ```, also on its own line -function CodeBlock(elem) - return pandoc.RawBlock('tex', '\\begin{myDisplay}\n' .. elem.text .. '\n\\end{myDisplay}') -end - diff --git a/pdf/codeblocks.lua b/pdf/codeblocks.lua deleted file mode 100644 index 26c26119..00000000 --- a/pdf/codeblocks.lua +++ /dev/null @@ -1,11 +0,0 @@ --- tested on pandoc 2.2.3.2 --- from agda doc: --- Code blocks start with ``` or ```agda on its own line, and end with ```, also on its own line -function CodeBlock(elem) - if #(elem.classes)==0 or elem.classes[1]=='agda' then - return pandoc.RawBlock('tex', '\\begin{fence}\n\\begin{code}\n' .. elem.text .. '\n\\end{code}\n\\end{fence}') - else - return pandoc.RawBlock('tex', '\\begin{myDisplay}\n' .. elem.text .. '\n\\end{myDisplay}') - end -end - diff --git a/pdf/handle-badges.lua b/pdf/handle-badges.lua deleted file mode 100644 index 854b3e51..00000000 --- a/pdf/handle-badges.lua +++ /dev/null @@ -1,5 +0,0 @@ -function Link(el) - if el.content[1].t == "Image" then - return pandoc.RawInline('markdown','') - end -end \ No newline at end of file diff --git a/pdf/lua/remove-badges.lua b/pdf/lua/remove-badges.lua new file mode 100644 index 00000000..69230ff0 --- /dev/null +++ b/pdf/lua/remove-badges.lua @@ -0,0 +1,12 @@ +function remove_badges(ln) + -- Remove link elements if their first child is a badge. + if #ln.content > 0 and ln.content[1].t == "Image" then + if string.match(ln.content[1].src, 'https://img%.shields%.io/badge/') then + return pandoc.Null() + end + end +end + +return { + { Link = remove_badges } +} diff --git a/pdf/rewrite-links.lua b/pdf/lua/rewrite-links.lua similarity index 100% rename from pdf/rewrite-links.lua rename to pdf/lua/rewrite-links.lua diff --git a/pdf/header-id.lua b/pdf/lua/single-file-headers-ids.lua similarity index 64% rename from pdf/header-id.lua rename to pdf/lua/single-file-headers-ids.lua index 3d707d5d..c5d09443 100644 --- a/pdf/header-id.lua +++ b/pdf/lua/single-file-headers-ids.lua @@ -3,20 +3,21 @@ -- Case 1: -- /title/: "Some Title" -- /permalink/: /Title/ -> # Some Title {#Title} +-- -- Case 2: -- ## Subsection Title {name=more-stuff} -> ## Subsection Title {#Title-more-stuff} +-- local identifier = nil local title = nil function get_identifier(meta) -- get title identifier from permalinks - for k,v in pairs(meta) do + for k,v in pairs(meta) do if k == "title" then - title = {table.unpack(v)} + title = {table.unpack(v)} end if k == "permalink" then - -- print(k,type(v[1].c)) -- set lower case permalink as identifier identifier = v[1].c:match("^/(%w+)/$") end @@ -25,25 +26,25 @@ end function insert_title(doc) -- insert title in front of the blocks - -- print(doc.blocks) - header = pandoc.Header(1,title) - header.identifier = identifier - -- print("header:" ,header.content) - table.insert(doc.blocks,1,header) + if title then + header = pandoc.Header(1,title) + header.identifier = identifier + table.insert(doc.blocks,1,header) + end return doc -end +end function change_identifier(elem) -- change header identifier based on metadata - local name = elem.attributes["name"] - if elem.t == "Header" and name then - -- can get labels - -- print(name, elem.identifier) + if elem.t == "Header" and name then elem.identifier = identifier .. "-" .. name - -- print(elem.identifier) end return elem end -return {{Meta=get_identifier}, {Header=change_identifier}, {Pandoc = insert_title}} \ No newline at end of file +return { + {Meta = get_identifier}, + {Header = change_identifier}, + {Pandoc = insert_title} +} diff --git a/pdf/lua/typeset-codeblocks.lua b/pdf/lua/typeset-codeblocks.lua new file mode 100644 index 00000000..e67f8244 --- /dev/null +++ b/pdf/lua/typeset-codeblocks.lua @@ -0,0 +1,49 @@ +local function typeset_codeblock(cb) + -- If a code block has class Agda or its class is omitted, format it as... + -- + -- \begin{agda}\begin{code} .. \end{agda}\end{code} + -- + -- ...otherwise, format it as... + -- + -- \begin{pre} .. \end{pre} + -- + -- Any file which is not checked by Agda must have its code blocks typeset in the latter style. + -- Specify these files via the UNCHECKED_FILES environment variable. + if is_checked() then + if #(cb.classes) == 0 or cb.classes[1] == 'agda' then + return pandoc.RawBlock('tex', '\\begin{agda}\n\\begin{code}\n' .. cb.text .. '\n\\end{code}\n\\end{agda}') + end + end + return pandoc.RawBlock('tex', '\\begin{pre}\n' .. cb.text .. '\n\\end{pre}') +end + +-- Set of unchecked files, where the names of unchecked files are stored in the table keys. +local UNCHECKED_FILES = nil + +-- Return whether the current file is checked by Agda, given by the UNCHECKED_FILES environment variable. +function is_checked() + + -- Initialise the table. + if UNCHECKED_FILES == nil then + UNCHECKED_FILES = {} + for unchecked_file in string.gmatch(pandoc.system.environment().UNCHECKED_FILES, "([^ ]+)") do + UNCHECKED_FILES[unchecked_file] = true + end + end + + -- Check if any of our input files is an unchecked file. + for _, input_file in pairs(PANDOC_STATE.input_files) do + if UNCHECKED_FILES[input_file] then + if #PANDOC_STATE.input_files > 1 then + error("Cannot handle multiple unchecked input files.") + else + return false + end + end + end + return true +end + +return { + { CodeBlock = typeset_codeblock } +} diff --git a/pdf/plfa-sample.tex b/pdf/plfa-sample.tex deleted file mode 100644 index a1a867fa..00000000 --- a/pdf/plfa-sample.tex +++ /dev/null @@ -1,171 +0,0 @@ -\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,fancyvrb,xcolor,tikz} -\tcbuselibrary{skins,breakable} -\usepackage{setspace} - -% wrap long texttt lines -\sloppy - -% disable section numbering -\setcounter{secnumdepth}{0} - - -% 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{bgcolor}{HTML}{EEEEFF} -\let\oldtexttt\texttt - -\renewcommand{\texttt}[1]{ - \colorbox{bgcolor}{\oldtexttt{#1}} - } - - -% indent verbatim to be the same as agda code blocks -\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt} - -% environments for adding background to agdacodeblocks and displays -\newtcolorbox{fence}[1][]{ - breakable, - colback=bgcolor, - spartan, - left=5pt, - boxrule=0pt, - frame hidden -} -\newenvironment{myDisplay} - {\VerbatimEnvironment - \begin{fence} - \begin{verbatim} - } - {\end{verbatim} - \end{fence} - } - - -\usepackage{geometry} - \geometry{ - a4paper, - total={170mm,257mm}, - left=20mm, - top=20mm, - } - - -% Use special font families without TeX ligatures for Agda code. (This -% code is inspired by a comment by Enrico Gregorio/egreg: -% 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{} - -\setlength{\parindent}{0em} -\setlength{\parskip}{1em} - - -% adjust spacing after toc numbering -\usepackage{tocloft} -\setlength\cftchapnumwidth{4em} - -% style links with colors instead of boxes -% https://tex.stackexchange.com/questions/823/remove-ugly-borders-around-clickable-cross-references-and-hyperlinks -\hypersetup{ - colorlinks, - linkcolor={red!50!black}, - citecolor={blue!50!black}, - urlcolor={blue!80!black} -} - -\begin{document} - -% adjust indentation of agda codeblocks -\setlength{\mathindent}{0pt} - -% Stack Overflow: (error) \tightlist (converting .md file into .pdf using pandoc) -% https://tex.stackexchange.com/questions/257418/error-tightlist-converting-md-file-into-pdf-using-pandoc/408474 -\providecommand{\tightlist}{% - \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} - -% https://ctan.org/pkg/titlepages -% https://latex.org/forum/viewtopic.php?t=2843 -\newlength{\drop} -\newcommand*{\titleAM}{\begingroup% Ancient Mariner, AW p. 151 -\setlength{\drop}{0.12\textheight} -\centering -\vspace*{\drop} -{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip] -\vspace*{\drop} -{\Huge Programming Language Foundations}\\[\baselineskip] -{\Huge in}\\[\baselineskip] -{\Huge Agda}\\[\drop] -% {\small\scshape the publisher}\par -\vfill -{\Large \scshape 2021}\par -\null\endgroup} - - - -\begin{titlepage} -\titleAM -\end{titlepage} -\frontmatter -\setcounter{tocdepth}{0} -\tableofcontents -\setcounter{tocdepth}{1} -\input{ latex/plfa/frontmatter/dedication } -\input{ latex/plfa/frontmatter/preface } -\input{ latex/plfa/frontmatter/README } - -\mainmatter -\part{Part 1: Logical Foundations} - \input{ latex/plfa/part1/Naturals } - \input{ latex/plfa/part1/Induction } - % \input{ latex/plfa/part1/Relations } - % \input{ latex/plfa/part1/Equality } - % \input{ latex/plfa/part1/Isomorphism } - % \input{ latex/plfa/part1/Connectives } - % \input{ latex/plfa/part1/Negation } - % \input{ latex/plfa/part1/Quantifiers } - % \input{ latex/plfa/part1/Decidable } - % \input{ latex/plfa/part1/Lists } -\part{Part 2: Programming Language Foundations} - \input{ latex/plfa/part2/Lambda} - % \input{ latex/plfa/part2/Properties} - \input{ latex/plfa/part2/DeBruijn} - % \input{ latex/plfa/part2/More} - % \input{ latex/plfa/part2/Bisimulation } - % \input{ latex/plfa/part2/Inference } - % \input{ latex/plfa/part2/Untyped } - % \input{ latex/plfa/part2/Confluence } - % \input{ latex/plfa/part2/BigStep } -\part{ Part 3: Denotational Semantics } - \input{ latex/plfa/part3/Denotational } - % \input{ latex/plfa/part3/Compositional } - % \input{ latex/plfa/part3/Soundness } - % \input{ latex/plfa/part3/Adequacy } - % \input{ latex/plfa/part3/ContextualEquivalence } - -% https://tex.stackexchange.com/questions/286431/putting-appendix-outside-the-last-part -\cleardoublepage -\phantomsection -\appendix -\addcontentsline{toc}{part}{Appendices} -% \input{ latex/plfa/part2/Substitution } -\input{ latex/plfa/backmatter/acknowledgements} -\input{ latex/plfa/backmatter/Fonts } -\end{document} \ No newline at end of file diff --git a/pdf/plfa.agda-lib b/pdf/plfa.agda-lib deleted file mode 100644 index 2e70e5a0..00000000 --- a/pdf/plfa.agda-lib +++ /dev/null @@ -1,3 +0,0 @@ -name: plfa -depend: standard-library -include: lagda_tex diff --git a/pdf/plfa.tex b/pdf/plfa.tex index 0568fb61..ea7cee46 100644 --- a/pdf/plfa.tex +++ b/pdf/plfa.tex @@ -1,4 +1,5 @@ \documentclass[10pt]{book} + \usepackage{hyperref} \usepackage[links]{agda} \usepackage{fontspec} @@ -6,50 +7,54 @@ \setsansfont{DejaVu Sans} \setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]} \usepackage{soul} -\usepackage{tcolorbox,fancyvrb,xcolor,tikz} +\usepackage[most]{tcolorbox} \tcbuselibrary{skins,breakable} +\usepackage{listings} +\usepackage{xcolor} +\usepackage{tikz} \usepackage{setspace} -% wrap texttt lines +% Wrap texttt lines \sloppy -% disable section numbering +% Disable section numbering \setcounter{secnumdepth}{0} - -% 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 - +% 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{bgcolor}{HTML}{EEEEFF} -\let\oldtexttt\texttt +\let\oldtexttt\texttt% +\renewcommand{\texttt}[1]{\colorbox{bgcolor}{\oldtexttt{#1}}} -\renewcommand{\texttt}[1]{ - \colorbox{bgcolor}{\oldtexttt{#1}} - } - - -% indent verbatim to be the same as agda code blocks -\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt} - -% environments for adding background to agdacodeblocks and displays -\newtcolorbox{fence}[1][]{ - breakable, +% Indent verbatim to be the same as agda code blocks. +\lstdefinestyle{codeBlockStyle}{ + basicstyle=\ttfamily, + numbers=none +} +\newtcolorbox{agda}[1][]{ + frame hidden, colback=bgcolor, spartan, left=5pt, boxrule=0pt, - frame hidden + breakable, +} +\newtcblisting{pre}{ + frame hidden, + colback=bgcolor, + spartan, + width=\textwidth, + listing only, + listing options={style=codeBlockStyle}, + arc=0mm, + top=0mm, + bottom=0mm, + left=0mm, + right=0mm, + boxrule=0pt, + breakable, } -\newenvironment{myDisplay} - {\VerbatimEnvironment - \begin{fence} - \begin{verbatim} - } - {\end{verbatim} - \end{fence} - } - \usepackage{geometry} \geometry{ @@ -57,16 +62,14 @@ total={170mm,257mm}, left=20mm, top=20mm, - } +} - - -% Use special font families without TeX ligatures for Agda code. (This -% code is inspired by a comment by Enrico Gregorio/egreg: -% https://tex.stackexchange.com/a/103078.) -\newfontfamily{\AgdaSerifFont}{DejaVu Serif} -\newfontfamily{\AgdaSansSerifFont}{DejaVu Sans} -\newfontfamily{\AgdaTypewriterFont}{DejaVu mononoki Symbola Droid} +% 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}} @@ -78,14 +81,13 @@ \setlength{\parindent}{0em} \setlength{\parskip}{1em} - -% adjust spacing after toc numbering +% Adjust spacing after toc numbering \usepackage{tocloft} \setlength\cftchapnumwidth{3em} \cftsetpnumwidth{4em} -% style links with colors instead of boxes -% https://tex.stackexchange.com/questions/823/remove-ugly-borders-around-clickable-cross-references-and-hyperlinks +% Style links with colors instead of boxes: +% https://tex.stackexchange.com/q/823 \hypersetup{ colorlinks, linkcolor={red!50!black}, @@ -95,79 +97,79 @@ \begin{document} -% adjust indentation of agda codeblocks +% Adjust indentation of agda codeblocks \setlength{\mathindent}{0pt} -% Stack Overflow: (error) \tightlist (converting .md file into .pdf using pandoc) -% https://tex.stackexchange.com/questions/257418/error-tightlist-converting-md-file-into-pdf-using-pandoc/408474 +% Provide \tightlist environment +% https://tex.stackexchange.com/q/257418 \providecommand{\tightlist}{% \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} % https://ctan.org/pkg/titlepages % https://latex.org/forum/viewtopic.php?t=2843 -\newlength{\drop} -\newcommand*{\titleAM}{\begingroup% Ancient Mariner, AW p. 151 -\setlength{\drop}{0.12\textheight} -\centering -\vspace*{\drop} -{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip] -\vspace*{\drop} -{\Huge Programming Language Foundations}\\[\baselineskip] -{\Huge in}\\[\baselineskip] -{\Huge Agda}\\[\drop] -% {\small\scshape the publisher}\par -\vfill -{\Large \scshape 2021}\par -\null\endgroup} - - \begin{titlepage} -\titleAM + \newlength{\drop} + \setlength{\drop}{0.12\textheight}% + \centering% + \begingroup% Ancient Mariner, AW p. 151 + \vspace*{\drop}% + {\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip] + {\Huge PROGRAMMING LANGUAGE FOUNDATIONS}\\[\baselineskip] + {\Large IN}\\[\baselineskip] + {\Huge Agda}\\[\drop] + \vfill% + {\small\scshape 2021}\par% + \null\endgroup \end{titlepage} + \frontmatter \setcounter{tocdepth}{0} + \tableofcontents \setcounter{tocdepth}{1} -\input{ latex/plfa/frontmatter/dedication } -\input{ latex/plfa/frontmatter/preface } -\input{ latex/plfa/frontmatter/README } +\input{plfa/frontmatter/dedication} +\input{plfa/frontmatter/preface} +\input{plfa/frontmatter/README} \mainmatter \part{Part 1: Logical Foundations} - \input{ latex/plfa/part1/Naturals } - \input{ latex/plfa/part1/Induction } - \input{ latex/plfa/part1/Relations } - \input{ latex/plfa/part1/Equality } - \input{ latex/plfa/part1/Isomorphism } - \input{ latex/plfa/part1/Connectives } - \input{ latex/plfa/part1/Negation } - \input{ latex/plfa/part1/Quantifiers } - \input{ latex/plfa/part1/Decidable } - \input{ latex/plfa/part1/Lists } -\part{Part 2: Programming Language Foundations} - \input{ latex/plfa/part2/Lambda} - \input{ latex/plfa/part2/Properties} - \input{ latex/plfa/part2/DeBruijn} - \input{ latex/plfa/part2/More} - \input{ latex/plfa/part2/Bisimulation } - \input{ latex/plfa/part2/Inference } - \input{ latex/plfa/part2/Untyped } - \input{ latex/plfa/part2/Confluence } - \input{ latex/plfa/part2/BigStep } -\part{ Part 3: Denotational Semantics } - \input{ latex/plfa/part3/Denotational } - \input{ latex/plfa/part3/Compositional } - \input{ latex/plfa/part3/Soundness } - \input{ latex/plfa/part3/Adequacy } - \input{ latex/plfa/part3/ContextualEquivalence } +\input{plfa/part1/Naturals} +\input{plfa/part1/Induction} +\input{plfa/part1/Relations} +\input{plfa/part1/Equality} +\input{plfa/part1/Isomorphism} +\input{plfa/part1/Connectives} +\input{plfa/part1/Negation} +\input{plfa/part1/Quantifiers} +\input{plfa/part1/Decidable} +\input{plfa/part1/Lists} + +\part{Part 2: Programming Language Foundations} +\input{plfa/part2/Lambda} +\input{plfa/part2/Properties} +\input{plfa/part2/DeBruijn} +\input{plfa/part2/More} +\input{plfa/part2/Bisimulation} +\input{plfa/part2/Inference} +\input{plfa/part2/Untyped} +\input{plfa/part2/Confluence} +\input{plfa/part2/BigStep} + +\part{Part 3: Denotational Semantics} +\input{plfa/part3/Denotational} +\input{plfa/part3/Compositional} +\input{plfa/part3/Soundness} +\input{plfa/part3/Adequacy} +\input{plfa/part3/ContextualEquivalence} + +\cleardoublepage% +\phantomsection% -% https://tex.stackexchange.com/questions/286431/putting-appendix-outside-the-last-part -\cleardoublepage -\phantomsection \appendix \addcontentsline{toc}{part}{Appendices} -\input{ latex/plfa/part2/Substitution } -\input{ latex/plfa/backmatter/acknowledgements} -\input{ latex/plfa/backmatter/Fonts } -\end{document} \ No newline at end of file + +\input{plfa/part2/Substitution} +\input{plfa/backmatter/acknowledgements} +\input{plfa/backmatter/Fonts} +\end{document} diff --git a/pdf/lagdamd2tex_acknowledgement.latex b/pdf/templates/acknowledgements.latex similarity index 100% rename from pdf/lagdamd2tex_acknowledgement.latex rename to pdf/templates/acknowledgements.latex diff --git a/pdf/lagdamd2tex_chapter.latex b/pdf/templates/chapter.latex similarity index 100% rename from pdf/lagdamd2tex_chapter.latex rename to pdf/templates/chapter.latex diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 8ba89a45..163ef41e 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -1012,7 +1012,7 @@ all-funs∈ {⊥} f with f {⊥} refl ... | fun () all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩ all-funs∈ {u ⊔ u′} f - with all-funs∈ λ z → f (inj₁ z) + with all-funs∈ (λ z → f (inj₁ z)) ... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩ ```