From 7130c6bd1124dd048d2ede082e3502d8924b8939 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 26 Dec 2024 12:35:03 -0800 Subject: [PATCH] Fix cross-linking in whitespace-trimmed files Signed-off-by: Danila Fedorin --- agda.rb | 10 +++++++++- themes/vanilla | 2 +- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/agda.rb b/agda.rb index d755641..85c06bd 100644 --- a/agda.rb +++ b/agda.rb @@ -160,6 +160,14 @@ class FileGroup line_range = 1.. end + # Sometimes, code is deeply nested in the source file, but we don't + # want to show the leading space. In that case, the generator sets + # data-source-offset with how much leading space was stripped off. + initial_offset = 0 + if source_offset_attr = t.attribute("data-source-offset") + initial_offset = source_offset_attr.to_s.to_i + end + full_path = t.attribute("data-file-path").to_s full_path_dirs = Pathname(full_path).each_filename.to_a @@ -195,7 +203,7 @@ class FileGroup line_info = agda_info[line_no] next unless line_info - offset = 0 + offset = initial_offset line.traverse do |lt| if lt.text? content = lt.content diff --git a/themes/vanilla b/themes/vanilla index 0cdd2fb..98a9d78 160000 --- a/themes/vanilla +++ b/themes/vanilla @@ -1 +1 @@ -Subproject commit 0cdd2fbf6484f994ebacac24020d510be7c56bb2 +Subproject commit 98a9d782730fd714ae7a3300d8cf6791ed0bc341