From 00f0f13b930a601ec9bdb7e571c5116b8ecc51bf Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 22 May 2024 22:29:26 -0700 Subject: [PATCH] Support cross-file linking Signed-off-by: Danila Fedorin --- agda.rb | 137 ++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 88 insertions(+), 49 deletions(-) diff --git a/agda.rb b/agda.rb index 512e2a7..77ff37f 100644 --- a/agda.rb +++ b/agda.rb @@ -11,7 +11,7 @@ class LineInfo end end -class Handler +class AgdaContext def initialize @file_infos = {} end @@ -71,16 +71,58 @@ class Handler href = at.attribute("href") id = at.attribute("id") if href or id - new_link = { :from => offset-at.content.length, :to => offset } - new_link[:href] = href if href - new_link[:id] = id if id + new_node = { :from => offset-at.content.length, :to => offset } + new_node[:href] = href if href + new_node[:id] = id if id - line_info.links << new_link + line_info.links << new_node end end end return line_infos end +end + +class FileGroup + def initialize(agda_context) + @agda_context = agda_context + # Agda HTML href -> list of (file, Hugo HTML node that links to it) + @nodes_referencing_href = {} + # Agda HTML href -> (its new ID in Hugo-land, file in which it's defined) + # This supports cross-post linking within a seires. + @global_seen_hrefs = {} + # file name -> Agda HTML href -> its new ID in Hugo-land + # This supports linking within a particular post. + @local_seen_hrefs = Hash.new { {} } + # Global counter to generate fresh IDs. There's no reason for it to + # be global within a series (since IDs are namespaced by the file they're in), + # but it's just more convenient this way. + @id_counter = 0 + end + + def note_defined_href(file, href) + file_hrefs = @local_seen_hrefs.fetch(file) do + @local_seen_hrefs[file] = {} + end + + uniq_id = file_hrefs.fetch(href) do + new_id = "agda-unique-ident-#{@id_counter}" + @id_counter += 1 + file_hrefs[href] = new_id + end + + unless @global_seen_hrefs.include? href + @global_seen_hrefs[href] = { :file => file, :id => uniq_id } + end + + return uniq_id + end + + def note_used_href(file, node, href) + ref_list = @nodes_referencing_href.fetch(href) { @nodes_referencing_href[href] = [] } + ref_list << { :file => file, :node => node } + return href + end # Given a Hugo HTML file which references potentially several Agda modules # in code blocks, insert links into the code blocks. @@ -100,13 +142,8 @@ class Handler # that are visible in the Hugo file, rename them to be globally unique, # and re-write cross-file links that reference these IDs to point # inside the Hugo file. - def process_source_file(file) - nodes_referencing_href = {} # Agda HTML ID -> all (Hugo HTML) nodes that link to it - seen_hrefs = {} # Agda HTML ID -> its new ID in Hugo-land - id_counter = 0 - + def process_source_file(file, document) # Process each highlight group that's been marked as an Agda file. - document = Nokogiri::HTML.parse(File.open(file)) document.css('div[data-agda-block]').each do |t| first_line, last_line = nil, nil @@ -148,7 +185,7 @@ class Handler html_file = dirs_in_base.join(".").gsub(/\.agda$/, ".html") html_path = File.join(["code", base_path, "html", html_file]) - agda_info = process_agda_html_file(html_path) + agda_info = @agda_context.process_agda_html_file(html_path) # Hugo conveniently generates a bunch of spans, each encoding a line # of code output. We can iterate over these and match them up with @@ -207,14 +244,12 @@ class Handler replace_with << content[replace_offset...relative_from] tag = (match.include? :href) ? 'a' : 'span' - new_link = Nokogiri::XML::Node.new(tag, document) + new_node = Nokogiri::XML::Node.new(tag, document) if match.include? :href # For nodes with links, note what they're referring to, so # we can adjust their hrefs when we assign global IDs. href = match[:href].to_s - new_link['href'] = href - ref_list = nodes_referencing_href.fetch(href) { nodes_referencing_href[href] = [] } - ref_list << new_link + new_node['href'] = note_used_href file, new_node, href end if match.include? :id # For nodes with IDs visible in the current Hugo file, we'll @@ -222,22 +257,11 @@ 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 - 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 + new_node['id'] = note_defined_href file, "#{html_file}##{id}" end - new_link.content = content[relative_from...relative_to] + new_node.content = content[relative_from...relative_to] - replace_with << new_link + replace_with << new_node replace_offset = relative_to end replace_with << content[replace_offset..-1] @@ -254,35 +278,50 @@ class Handler end end end + end + def cross_link_files(file_documents) # Now, we have a complete list of all the IDs visible in scope. # Redirect relevant links to these IDs. This achieves within-post # links. - seen_hrefs.each do |agda_id, hugo_id| - nodes_to_rewrite = nodes_referencing_href[agda_id] - next unless nodes_to_rewrite + @nodes_referencing_href.each do |href, references| + references.each do |reference| + file = reference[:file] + node = reference[:node] - nodes_to_rewrite.each do |node| - node['href'] = "##{hugo_id}" - end + local_targets = @local_seen_hrefs[file] + if local_targets.include? href + # A code block in this fine provides this href, create a local link. + node['href'] = "##{local_targets[href]}" + elsif @global_seen_hrefs.include? href + # A code block in this series, but not in this file, defines + # this href. Create a cross-file link. + target = @global_seen_hrefs[href] + other_file = target[:file] + id = target[:id] - nodes_referencing_href.delete agda_id - end - - # The remaining nodes reference symbols not in the current Hugo document, - # so just replace them with their contents for now (we'd need some - # external hosting to make this work otherwise). - nodes_referencing_href.each do |href, nodes| - nodes.each do |node| - node.replace node.content + relpath = Pathname.new(other_file).dirname.relative_path_from(Pathname.new(file).dirname) + puts relpath + node['href'] = "#{relpath}##{id}" + else + # No definitions in any blog page. For now, just delete the anchor. + node.replace node.content + end end end - - File.write(file, document.to_html(encoding: 'UTF-8')) end end -handler = Handler.new +agda_context = AgdaContext.new +file_documents = {} files.each do |file| - handler.process_source_file file + file_documents[file] = document = Nokogiri::HTML.parse(File.open(file)) +end +handler = FileGroup.new agda_context +file_documents.each do |file, document| + handler.process_source_file file, document +end +handler.cross_link_files(file_documents) +file_documents.each do |file, document| + File.write(file, document.to_html(encoding: 'UTF-8')) end