Support cross-file linking

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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_node = { :from => offset-at.content.length, :to => offset }
-          new_link[:href] = href if href
+          new_node[:href] = href if href
-          new_link[:id] = id if id
+          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)
+  def process_source_file(file, document)
-    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
-
     # 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
+                new_node['href'] = note_used_href file, new_node, href
-                ref_list = nodes_referencing_href.fetch(href) { nodes_referencing_href[href] = [] }
-                ref_list << new_link
               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}"
+                new_node['id'] = note_defined_href file, "#{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.content = content[relative_from...relative_to]
-              end
-              new_link.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_referencing_href.each do |href, references|
-      nodes_to_rewrite = nodes_referencing_href[agda_id]
+      references.each do |reference|
-      next unless nodes_to_rewrite
+        file = reference[:file]
+        node = reference[:node]
 
-      nodes_to_rewrite.each do |node|
+        local_targets = @local_seen_hrefs[file]
-        node['href'] = "##{hugo_id}"
+        if local_targets.include? href
-      end
+          # 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
+          relpath = Pathname.new(other_file).dirname.relative_path_from(Pathname.new(file).dirname)
-    end
+          puts relpath
-
+          node['href'] = "#{relpath}##{id}"
-    # The remaining nodes reference symbols not in the current Hugo document,
+        else
-    # so just replace them with their contents for now (we'd need some
+          # No definitions in any blog page. For now, just delete the anchor.
-    # external hosting to make this work otherwise).
-    nodes_referencing_href.each do |href, nodes|
-      nodes.each do |node|
           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