Fix cross-linking in whitespace-trimmed files
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
c5aacc060a
commit
7130c6bd11
10
agda.rb
10
agda.rb
@ -160,6 +160,14 @@ class FileGroup
|
|||||||
line_range = 1..
|
line_range = 1..
|
||||||
end
|
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 = t.attribute("data-file-path").to_s
|
||||||
full_path_dirs = Pathname(full_path).each_filename.to_a
|
full_path_dirs = Pathname(full_path).each_filename.to_a
|
||||||
|
|
||||||
@ -195,7 +203,7 @@ class FileGroup
|
|||||||
line_info = agda_info[line_no]
|
line_info = agda_info[line_no]
|
||||||
next unless line_info
|
next unless line_info
|
||||||
|
|
||||||
offset = 0
|
offset = initial_offset
|
||||||
line.traverse do |lt|
|
line.traverse do |lt|
|
||||||
if lt.text?
|
if lt.text?
|
||||||
content = lt.content
|
content = lt.content
|
||||||
|
@ -1 +1 @@
|
|||||||
Subproject commit 0cdd2fbf6484f994ebacac24020d510be7c56bb2
|
Subproject commit 98a9d782730fd714ae7a3300d8cf6791ed0bc341
|
Loading…
Reference in New Issue
Block a user