From 5e117e3f485c305ee7a297c2e95cd53d8f52e248 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 4 Jan 2026 16:33:43 -0800 Subject: [PATCH] Ignore warnings encoded as syntax highlighting Signed-off-by: Danila Fedorin --- agda.rb | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/agda.rb b/agda.rb index 48a83df..7932e34 100644 --- a/agda.rb +++ b/agda.rb @@ -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 \n 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