michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add EPUB creation to the build

Browse source 
The EPUB is created with `pandoc` in combination with Lua filters, which
rewrite the abstract syntax tree to be more suitable for EPUB creation.
In particular all headings in the markdown files `part[123]/*.lagda.md`
are shifted up by 1 (e.g., level 1 heading -> level 2 heading), so that
we can make a level 1 heading for Appendix, Frontmatter, and different
parts of the book. This is done to match the structure on the website [1].

Syntax highlighting is done using pandoc's builtin syntax highlighter
(which uses the Haskell library `skylighting`). In other words, we do
not use `highlight.sh`, so the syntax highlighting is slightly different
than the website version of the book. This could certainly be dealt with
later.

What follows is a list of things that are currently broken, which is
probably not exhaustive:
- The `Acknowledgements` section is broken.
- Embedded fonts don't work. They're necessary for some ereaders, like my old Sony PRS-300.
- All inline links are broken. I could rewrite them with a Lua filter
  and some regex, although that's not very nice :)
- `epubcheck` validation fails for a variety of reasons.

Closes #112.

[1]: https://plfa.github.io/
[2]: https://github.com/w3c/epubcheck
This commit is contained in:
Michael Reed 2020-06-07 20:45:49 -04:00
parent 44fb26193f
commit 55c7a10e23
13 changed files with 620 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
.gitignore vendored
View file

@ -21,5 +21,8 @@ Gemfile.lock
*.spl
*.synctex.gz
## EPUB files
*.epub
## Emacs files
auto/
auto/

BIN
DejaVuSansMono.ttf Normal file
View file

Binary file not shown.

33
Makefile
View file

@ -35,6 +35,35 @@ statistics:
out/:
mkdir -p out/
# EPUB generation notes
#
# - The "Apple Books" app on Mac does not show syntax highlighting.
# The Thorium app on Mac, however, does.
#
# - Regarding --epub-chapter-level, from the docs (https://pandoc.org/MANUAL.html):
#
# "Specify the heading level at which to split the EPUB into separate “chapter”
# files. The default is to split into chapters at level-1 headings. This option
# only affects the internal composition of the EPUB, not the way chapters and
# sections are displayed to users. Some readers may be slow if the chapter
# files are too large, so for large documents with few level-1 headings, one
# might want to use a chapter level of 2 or 3."
#
#TODO: embedded fonts not working (path problem?)
epub: out/
pandoc --strip-comments \
--css=epub.css \
--epub-embed-font=DejaVuSansMono.ttf \
--lua-filter include-files.lua \
--lua-filter default-code-class.lua -M default-code-class=agda \
--standalone \
--toc --toc-depth=2 \
--epub-chapter-level=2 \
-o out/plfa.epub \
index_epub.md
# Convert literal Agda to Markdown
define AGDA_template
@ -82,7 +111,7 @@ build-incremental: $(MARKDOWN)
# Remove all auxiliary files
clean:
rm -f .agda-stdlib.sed .links-*.sed
rm -f .agda-stdlib.sed .links-*.sed out/plfa.epub
ifneq ($(strip $(AGDAI)),)
rm $(AGDAI)
endif
@ -185,4 +214,4 @@ travis-uninstall-agda-stdlib:
travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub

26
default-code-class.lua Normal file
View file

@ -0,0 +1,26 @@
-- Source:
-- https://github.com/jgm/pandoc/issues/2104#issuecomment-595878750
--
-- Assign a code class to all code blocks lacking one. Unlike the
-- command-line flag "--indented-code-classes", which only applies
-- to indented code blocks, this lua filter applies to all inline
-- code elements, including fenced code blocks.
local default_code_classes = {}
function add_default_code_class(el)
if #(el.classes) == 0 then
el.classes = default_code_classes
return el
end
end
function get_default_code_class(meta)
if meta['default-code-class'] then
default_code_classes = {pandoc.utils.stringify(meta['default-code-class'])}
end
end
return {{Meta = get_default_code_class},
{Code = add_default_code_class},
{CodeBlock = add_default_code_class}}

51
epub.css Normal file
View file

@ -0,0 +1,51 @@
/* This is Pandoc's default ebook CSS, modified slightly. */
/* https://github.com/jgm/pandoc/blob/master/data/epub.css */
@font-face {
font-family: 'mononoki';
font-weight: normal;
font-style: normal;
src: url('fonts/mononoki-Regular.ttf');
}
@font-face {
font-family: 'DejaVu Sans Mono';
font-weight: normal;
font-style: normal;
src: url('fonts/DejaVuSansMono.ttf');
}
@font-face {
font-family: 'Source Code Pro';
font-weight: normal;
font-style: normal;
src: url('fonts/SourceCodePro-Regular.ttf');
}
/* TODO: add freemono font from agda.css */
body { margin: 5%; text-align: justify; font-size: medium; }
code { font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', monospace; }
h1 { text-align: left; }
h2 { text-align: left; }
h3 { text-align: left; }
h4 { text-align: left; }
h5 { text-align: left; }
h6 { text-align: left; }
h1.title { }
h2.author { }
h3.date { }
nav#toc ol,
nav#landmarks ol { padding: 0; margin-left: 1em; }
nav#toc ol li,
nav#landmarks ol li { list-style-type: none; margin: 0; padding: 0; }
a.footnote-ref { vertical-align: super; }
em, em em em, em em em em em { font-style: italic;}
em em, em em em em { font-style: normal; }
code{ white-space: pre-wrap; }
span.smallcaps{ font-variant: small-caps; }
span.underline{ text-decoration: underline; }
q { quotes: "“" "”" "‘" "’"; }
div.column{ display: inline-block; vertical-align: top; width: 50%; }
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
@media screen { /* Workaround for iBooks issue; see #6242 */
.sourceCode {
overflow: visible !important;
white-space: pre-wrap !important;
}
}

BIN
fonts/DejaVuSansMono.ttf Normal file
View file

Binary file not shown.

187
fonts/LICENSE_dejavu.txt Normal file
View file

@ -0,0 +1,187 @@
Fonts are (c) Bitstream (see below). DejaVu changes are in public domain.
Glyphs imported from Arev fonts are (c) Tavmjong Bah (see below)
Bitstream Vera Fonts Copyright
------------------------------
Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera is
a trademark of Bitstream, Inc.
Permission is hereby granted, free of charge, to any person obtaining a copy
of the fonts accompanying this license ("Fonts") and associated
documentation files (the "Font Software"), to reproduce and distribute the
Font Software, including without limitation the rights to use, copy, merge,
publish, distribute, and/or sell copies of the Font Software, and to permit
persons to whom the Font Software is furnished to do so, subject to the
following conditions:
The above copyright and trademark notices and this permission notice shall
be included in all copies of one or more of the Font Software typefaces.
The Font Software may be modified, altered, or added to, and in particular
the designs of glyphs or characters in the Fonts may be modified and
additional glyphs or characters may be added to the Fonts, only if the fonts
are renamed to names not containing either the words "Bitstream" or the word
"Vera".
This License becomes null and void to the extent applicable to Fonts or Font
Software that has been modified and is distributed under the "Bitstream
Vera" names.
The Font Software may be sold as part of a larger software package but no
copy of one or more of the Font Software typefaces may be sold by itself.
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING
ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES,
WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE
FONT SOFTWARE.
Except as contained in this notice, the names of Gnome, the Gnome
Foundation, and Bitstream Inc., shall not be used in advertising or
otherwise to promote the sale, use or other dealings in this Font Software
without prior written authorization from the Gnome Foundation or Bitstream
Inc., respectively. For further information, contact: fonts at gnome dot
org.
Arev Fonts Copyright
------------------------------
Copyright (c) 2006 by Tavmjong Bah. All Rights Reserved.
Permission is hereby granted, free of charge, to any person obtaining
a copy of the fonts accompanying this license ("Fonts") and
associated documentation files (the "Font Software"), to reproduce
and distribute the modifications to the Bitstream Vera Font Software,
including without limitation the rights to use, copy, merge, publish,
distribute, and/or sell copies of the Font Software, and to permit
persons to whom the Font Software is furnished to do so, subject to
the following conditions:
The above copyright and trademark notices and this permission notice
shall be included in all copies of one or more of the Font Software
typefaces.
The Font Software may be modified, altered, or added to, and in
particular the designs of glyphs or characters in the Fonts may be
modified and additional glyphs or characters may be added to the
Fonts, only if the fonts are renamed to names not containing either
the words "Tavmjong Bah" or the word "Arev".
This License becomes null and void to the extent applicable to Fonts
or Font Software that has been modified and is distributed under the
"Tavmjong Bah Arev" names.
The Font Software may be sold as part of a larger software package but
no copy of one or more of the Font Software typefaces may be sold by
itself.
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL
TAVMJONG BAH BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.
Except as contained in this notice, the name of Tavmjong Bah shall not
be used in advertising or otherwise to promote the sale, use or other
dealings in this Font Software without prior written authorization
from Tavmjong Bah. For further information, contact: tavmjong @ free
. fr.
TeX Gyre DJV Math
-----------------
Fonts are (c) Bitstream (see below). DejaVu changes are in public domain.
Math extensions done by B. Jackowski, P. Strzelczyk and P. Pianowski
(on behalf of TeX users groups) are in public domain.
Letters imported from Euler Fraktur from AMSfonts are (c) American
Mathematical Society (see below).
Bitstream Vera Fonts Copyright
Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera
is a trademark of Bitstream, Inc.
Permission is hereby granted, free of charge, to any person obtaining a copy
of the fonts accompanying this license (“Fonts”) and associated
documentation
files (the “Font Software”), to reproduce and distribute the Font Software,
including without limitation the rights to use, copy, merge, publish,
distribute,
and/or sell copies of the Font Software, and to permit persons to whom
the Font Software is furnished to do so, subject to the following
conditions:
The above copyright and trademark notices and this permission notice
shall be
included in all copies of one or more of the Font Software typefaces.
The Font Software may be modified, altered, or added to, and in particular
the designs of glyphs or characters in the Fonts may be modified and
additional
glyphs or characters may be added to the Fonts, only if the fonts are
renamed
to names not containing either the words “Bitstream” or the word “Vera”.
This License becomes null and void to the extent applicable to Fonts or
Font Software
that has been modified and is distributed under the “Bitstream Vera”
names.
The Font Software may be sold as part of a larger software package but
no copy
of one or more of the Font Software typefaces may be sold by itself.
THE FONT SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS
OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
FOUNDATION
BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL,
SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN
ACTION
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR
INABILITY TO USE
THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.
Except as contained in this notice, the names of GNOME, the GNOME
Foundation,
and Bitstream Inc., shall not be used in advertising or otherwise to promote
the sale, use or other dealings in this Font Software without prior written
authorization from the GNOME Foundation or Bitstream Inc., respectively.
For further information, contact: fonts at gnome dot org.
AMSFonts (v. 2.2) copyright
The PostScript Type 1 implementation of the AMSFonts produced by and
previously distributed by Blue Sky Research and Y&Y, Inc. are now freely
available for general use. This has been accomplished through the
cooperation
of a consortium of scientific publishers with Blue Sky Research and Y&Y.
Members of this consortium include:
Elsevier Science IBM Corporation Society for Industrial and Applied
Mathematics (SIAM) Springer-Verlag American Mathematical Society (AMS)
In order to assure the authenticity of these fonts, copyright will be
held by
the American Mathematical Society. This is not meant to restrict in any way
the legitimate use of the fonts, such as (but not limited to) electronic
distribution of documents containing these fonts, inclusion of these fonts
into other public domain or commercial font collections or computer
applications, use of the outline data to create derivative fonts and/or
faces, etc. However, the AMS does require that the AMS copyright notice be
removed from any derivative versions of the fonts which have been altered in
any way. In addition, to ensure the fidelity of TeX documents using Computer
Modern fonts, Professor Donald Knuth, creator of the Computer Modern faces,
has requested that any alterations which yield different font metrics be
given a different name.
$Id$

94
fonts/LICENSE_mononoki.txt Normal file
View file

@ -0,0 +1,94 @@
Copyright (c) 2013, Matthias Tellen matthias.tellen@googlemail.com,
with Reserved Font Name monoOne.
This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at:
http://scripts.sil.org/OFL
-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------
PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.
The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded,
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.
DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.
"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).
"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).
"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.
"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.
PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:
1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.
2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.
3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.
5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.
TERMINATION
This license becomes null and void if any of the above conditions are
not met.
DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.

93
fonts/LICENSE_source_code_pro.txt Executable file
View file

@ -0,0 +1,93 @@
Copyright 2010, 2012 Adobe Systems Incorporated (http://www.adobe.com/), with Reserved Font Name 'Source'. All Rights Reserved. Source is a trademark of Adobe Systems Incorporated in the United States and/or other countries.
This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL
-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------
PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.
The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded,
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.
DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.
"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).
"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).
"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.
"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.
PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:
1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.
2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.
3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.
5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.
TERMINATION
This license becomes null and void if any of the above conditions are
not met.
DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.

BIN
fonts/SourceCodePro-Regular.ttf Normal file
View file

Binary file not shown.

BIN
fonts/mononoki-Regular.ttf Normal file
View file

Binary file not shown.

61
include-files.lua Normal file
View file

@ -0,0 +1,61 @@
--- include-files.lua – filter to include Markdown files
---
--- Copyright: © 2019–2020 Albert Krewinkel
--- Copyright: © 2020 Michael Reed
--- License: MIT – see LICENSE file for details
---
--- Created by Albert Krewinkel. Slightly modified by Michael Reed for use in
--- generating the EPUB for "Programming Language Foundations in Agda".
---
--- For documentation, see: https://github.com/pandoc/lua-filters/tree/master/include-files
-- pandoc's List type
local List = require 'pandoc.List'
--- Shift headings in block list by given number
function shift_headings(blocks, shift_by)
if not shift_by then
return blocks
end
local shift_headings_filter = {
Header = function (header)
header.level = header.level + shift_by
return header
end
}
return pandoc.walk_block(pandoc.Div(blocks), shift_headings_filter).content
end
--- Filter function for code blocks
function CodeBlock(cb)
-- ignore code blocks which are not of class "include".
if not cb.classes:includes 'include' then
return
end
-- Markdown is used if this is nil.
local format = cb.attributes['format']
local shift_heading_level_by =
tonumber(cb.attributes['shift-heading-level-by'])
local blocks = List:new()
for line in cb.text:gmatch('[^\n]+') do
if line:sub(1,2) ~= '//' then
-- Read in the document at the file path specified by `line`.
local fh = io.open(line)
local document = pandoc.read(fh:read '*a', format)
-- Before shifting headings, add a title heading at the beginning of the chapter.
local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title)))
document.blocks:insert(1, heading)
-- Shift all headings by the user-specified amount, which is 0 by default.
local chapter = shift_headings(document.blocks, shift_heading_level_by)
-- Concatenate the chapter blocks (discarding the metadata) to the current document.
blocks:extend(chapter)
fh:close()
end
end
return blocks
end

73
index_epub.md Normal file
View file

@ -0,0 +1,73 @@
---
title: Programming Language Foundations in Agda
author:
- Philip Wadler
- Wen Kokke
- Jeremy G. Siek
description: This book is an introduction to programming language theory using the proof assistant Agda.
rights: Creative Commons Attribution 4.0 International License
language: en-US
---
# Front matter
``` {.include shift-heading-level-by=1}
src/plfa/dedication.md
src/plfa/preface.md
```
# Part 1: Logical Foundations
``` {.include shift-heading-level-by=1}
src/plfa/part1/Naturals.lagda.md
src/plfa/part1/Induction.lagda.md
src/plfa/part1/Relations.lagda.md
src/plfa/part1/Equality.lagda.md
src/plfa/part1/Isomorphism.lagda.md
src/plfa/part1/Connectives.lagda.md
src/plfa/part1/Negation.lagda.md
src/plfa/part1/Quantifiers.lagda.md
src/plfa/part1/Decidable.lagda.md
src/plfa/part1/Lists.lagda.md
```
# Part 2: Operational Semantics
``` {.include shift-heading-level-by=1}
src/plfa/part2/Lambda.lagda.md
src/plfa/part2/Properties.lagda.md
src/plfa/part2/DeBruijn.lagda.md
src/plfa/part2/More.lagda.md
src/plfa/part2/Bisimulation.lagda.md
src/plfa/part2/Inference.lagda.md
src/plfa/part2/Untyped.lagda.md
src/plfa/part2/Confluence.lagda.md
src/plfa/part2/BigStep.lagda.md
```
# Part 3: Denotational Semantics
``` {.include shift-heading-level-by=1}
src/plfa/part3/Denotational.lagda.md
src/plfa/part3/Compositional.lagda.md
src/plfa/part3/Soundness.lagda.md
src/plfa/part3/Adequacy.lagda.md
src/plfa/part3/ContextualEquivalence.lagda.md
```
# Appendix
``` {.include shift-heading-level-by=1}
src/plfa/part2/Substitution.lagda.md
```
# Backmatter
``` {.include shift-heading-level-by=1}
src/plfa/acknowledgements.md
src/plfa/Fonts.lagda.md
src/plfa/statistics.md
```
<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->