4 Commits

Author SHA1 Message Date
4d35ca04fe Slightly tweak wording
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-01-19 10:23:02 -08:00
5e117e3f48 Ignore warnings encoded as syntax highlighting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-01-04 16:33:43 -08:00
a6f3cd3f9a Update theme.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-01-03 18:08:51 -08:00
ccc8d6f0eb Re-enable hiding LaTeX
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-01-03 16:34:57 -08:00
4 changed files with 18 additions and 9 deletions

12
agda.rb
View File

@@ -46,7 +46,17 @@ class AgdaContext
# assumes that links can't span multiple pages, and that links
# aren't nested, so ensure that the parent of the textual node
# is the preformatted block itself.
raise "unsupported Agda HTML output" if at.parent.name != "pre"
if at.parent.name != "pre"
# Costmetic highlight warnings are sometimes applied to newlines.
# If they don't have content, treat them as normal newlines at the
# top level.
#
# This is an <a class="CosmeticProblem">\n</a> node.
unless at.parent.name == "a" and at.parent['class'] == "CosmeticProblem" and at.content.strip.empty?
raise "unsupported Agda HTML output in file #{file} at line #{line} (content #{at.content.inspect})"
end
end
# Increase the line and track the final offset. Written as a loop
# in case we eventually want to add some handling for the pieces

View File

@@ -412,4 +412,4 @@ ideas to absurd and humorous extremes. So, my final reason:
kind, welcoming and enthusiastic people, who dedicate much of their
time to spreading the joy of the field.
I ❤️ you.
I ❤️ the programming languages community.

View File

@@ -68,13 +68,12 @@ files.each do |file|
t.replace(rendered)
end
found_any ||= document.at('meta[name="needs-latex"]')
# If we didn't find any mathematical equations, no need to include KaTeX CSS.
# Disabled here because Bergamot technically doesn't require math blocks
# on the page but does need the CSS.
#
# unless found_any
# document.css('link[href$="katex.css"], link[href$="katex.min.css"]').each(&:remove)
# end
unless found_any
document.css('link[href$="katex.css"], link[href$="katex.min.css"]').each(&:remove)
end
File.write(file, document.to_html(encoding: 'UTF-8'))
end