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 # assumes that links can't span multiple pages, and that links
# aren't nested, so ensure that the parent of the textual node # aren't nested, so ensure that the parent of the textual node
# is the preformatted block itself. # 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 # Increase the line and track the final offset. Written as a loop
# in case we eventually want to add some handling for the pieces # 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 kind, welcoming and enthusiastic people, who dedicate much of their
time to spreading the joy of the field. 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) t.replace(rendered)
end end
found_any ||= document.at('meta[name="needs-latex"]')
# If we didn't find any mathematical equations, no need to include KaTeX CSS. # If we didn't find any mathematical equations, no need to include KaTeX CSS.
# Disabled here because Bergamot technically doesn't require math blocks unless found_any
# on the page but does need the CSS. 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')) File.write(file, document.to_html(encoding: 'UTF-8'))
end end