Improve support when code occurrs multiple times
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
		
							parent
							
								
									f78f877e21
								
							
						
					
					
						commit
						9d0dcd98bd
					
				
							
								
								
									
										14
									
								
								agda.rb
									
									
									
									
									
								
							
							
						
						
									
										14
									
								
								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] | ||||
| 
 | ||||
|  | ||||
		Loading…
	
		Reference in New Issue
	
	Block a user