EPUB: Fix broken links

This is done with a lua filter that rewrites links with regular
expressions.

References #480.
This commit is contained in:
Michael Reed 2020-06-17 19:38:26 -04:00
parent b2b8b324af
commit 75654740b3
3 changed files with 45 additions and 1 deletions

View file

@ -61,6 +61,7 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
--epub-embed-font='assets/fonts/FreeMono.woff' \
--epub-embed-font='assets/fonts/DejaVuSansMono.woff' \
--lua-filter epub/include-files.lua \
--lua-filter epub/rewrite-links.lua \
--lua-filter epub/default-code-class.lua -M default-code-class=agda \
--standalone \
--fail-if-warnings \

43
epub/rewrite-links.lua Normal file
View file

@ -0,0 +1,43 @@
local currentChapter = nil
-- Reassigns identifiers for all all Headers level 2 and higher. Level 2 Headers
-- correspond to chapters, and are identified by the first word in their content
-- field. Headers of level more than 2 are identified by "#<chapter>-<anchor>",
-- where "<chapter>" is the identifier of the chapter this header is nested in,
-- and "<anchor>" is this Header's existing identifier.
function Header (el)
if el.level == 2 then
local title = pandoc.utils.stringify(el.content[1])
currentChapter = title:match("%w+")
el.identifier = currentChapter
elseif el.level > 2 then
el.identifier = currentChapter .. '-' .. el.identifier
end
return el
end
-- Performs the following transformations on Link targets:
--
-- Case 1:
-- [text]({{ site.baseurl }}/chapter/#more-stuff) -> [text](#chapter-more-stuff)
--
-- Case 2:
-- [text]({{ site.baseurl }}/chapter/) -> [text](#stuff)
--
-- All other Links are ignored.
function Link (el)
local n
-- When parsing a markdown link such as "[stuff]({{ site.baseurl }}/Naturals",
-- pandoc encodes the link's URL with percent-encoding, resulting in the
-- link "[stuff](%7B%7B+site.baseurl+%7D%7D%2FNaturals)". This is why the
-- pattern begins with ".*site%.baseurl.*" and not "{{ site%.baseurl }}".
el.target, n = el.target:gsub("^.*site%.baseurl.*/(%w+)/#([%w-]+)$", -- case 1
"#%1-%2")
if n == 0 then
el.target = el.target:gsub("^.*site%.baseurl.*/(%w+)/$", -- case 2
"#%1")
end
return el
end

View file

@ -1234,7 +1234,7 @@ side to be well typed.
## Test examples
We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn),
We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
in order to make sure we have not broken anything in the process of extending our base calculus.
```
two : ∀ {Γ} → Γ ⊢ `