Merge pull request #481 from mreed20/rewrite-links
EPUB: Fix broken links
This commit is contained in:
commit
9a8f8c1bb2
3 changed files with 45 additions and 1 deletions
1
Makefile
1
Makefile
|
@ -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
43
epub/rewrite-links.lua
Normal 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](#chapter)
|
||||
--
|
||||
-- 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%20site.baseurl%20%7D%7D/Naturals)".
|
||||
local baseurl = "%%7B%%7B%%20site%.baseurl%%20%%7D%%7D"
|
||||
el.target, n = el.target:gsub("^" .. baseurl .. "/(%w+)/#([%w-]+)$", -- case 1
|
||||
"#%1-%2")
|
||||
if n == 0 then
|
||||
el.target = el.target:gsub("^" .. baseurl .. "/(%w+)/$", -- case 2
|
||||
"#%1")
|
||||
end
|
||||
return el
|
||||
end
|
|
@ -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 : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
|
|
Loading…
Add table
Reference in a new issue