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]