Ignore warnings encoded as syntax highlighting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
12
agda.rb
12
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 <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
|
||||
|
||||
Reference in New Issue
Block a user