From 9d0dcd98bd91ac2927083047fbed007704a137e2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 22 May 2024 17:05:38 -0700 Subject: [PATCH] Improve support when code occurrs multiple times Signed-off-by: Danila Fedorin --- agda.rb | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/agda.rb b/agda.rb index c0dfcad..512e2a7 100644 --- a/agda.rb +++ b/agda.rb @@ -222,10 +222,18 @@ class Handler # module HTML files. So, note the ID that we want to redirect, # and pick a new unique ID to replace it with. id = match[:id].to_s - uniq_id = "agda-unique-ident-#{id_counter}" - id_counter += 1 + local_href = "#{html_file}##{id}" + + # The same piece of Agda module code could have been included + # twice (e.g., a snippet first, then the surrounding code) + # In that case, don't assign it a new ID; prefer the earlier + # occurrence. + uniq_id = seen_hrefs.fetch(local_href) do + new_id = "agda-unique-ident-#{id_counter}" + id_counter += 1 + seen_hrefs[local_href] = new_id + end new_link['id'] = uniq_id - seen_hrefs["#{html_file}##{id}"] = uniq_id end new_link.content = content[relative_from...relative_to]