From 8ad83631c5fbca69ef2be93767bdf471bcb28dc8 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 11 Sep 2024 13:47:09 +0200 Subject: [PATCH] Use correct line_start in diagnostic range snippet. --- hax-types/src/diagnostics/report.rs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs index 3faba540d..cf84959b6 100644 --- a/hax-types/src/diagnostics/report.rs +++ b/hax-types/src/diagnostics/report.rs @@ -74,20 +74,21 @@ impl Diagnostics { let start = compute_offset(&source, span.lo.line, span.lo.col); let end = compute_offset(&source, span.hi.line, span.hi.col); let origin = format!("{}", path.display()); - snippets_data.push((source, origin, span.lo.line, start..end)); + snippets_data.push((source, origin, start..end)); }; } let title = format!("[{}] {self}", self.kind.code()); - let message = level.title(&title).snippets(snippets_data.iter().map( - |(source, origin, line, range)| { - Snippet::source(source) - .line_start(*line) - .origin(&origin) - .fold(true) - .annotation(level.span(range.clone())) - }, - )); + let message = + level + .title(&title) + .snippets(snippets_data.iter().map(|(source, origin, range)| { + Snippet::source(source) + .line_start(1) + .origin(&origin) + .fold(true) + .annotation(level.span(range.clone())) + })); then(message) }