Support non-submodule code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
032411fe9c
commit
5d0b903c03
26
agda.rb
26
agda.rb
|
@ -117,16 +117,28 @@ class Handler
|
|||
last_line = last_line_attr.to_s.to_i
|
||||
end
|
||||
|
||||
# The name of an Agda module is determined from its directory
|
||||
# structure: A/B/C.agda creates A.B.C.html. Assume that the
|
||||
# base path is the Agda module root, and use the remaining directories
|
||||
# to build the HTML file name.
|
||||
base_path = t.attribute("data-base-path").to_s
|
||||
base_path_dirs = Pathname(base_path).each_filename.to_a
|
||||
full_path = t.attribute("data-file-path").to_s
|
||||
full_path_dirs = Pathname(full_path).each_filename.to_a
|
||||
|
||||
dirs_in_base = full_path_dirs[base_path_dirs.length..-1]
|
||||
# The name of an Agda module is determined from its directory
|
||||
# structure: A/B/C.agda creates A.B.C.html. Depending on where
|
||||
# the code is included, there might be some additional folders
|
||||
# that precede A that we want to ignore.
|
||||
base_path = t.attribute("data-base-path").to_s
|
||||
base_dir_depth = 0
|
||||
if base_path.empty?
|
||||
# No submodules were used. Assume code/<X> is the root, since
|
||||
# that's the code layout of the blog right now.
|
||||
base_dir_depth = 1
|
||||
base_path = full_path_dirs[0]
|
||||
else
|
||||
# The code is in a submodule. Assume that the base path / submodule
|
||||
# root is the Agda module root, ignore all folders before that.
|
||||
base_path_dirs = Pathname(base_path).each_filename.to_a
|
||||
base_dir_depth = base_path_dirs.length
|
||||
end
|
||||
|
||||
dirs_in_base = full_path_dirs[base_dir_depth..-1]
|
||||
html_file = dirs_in_base.join(".").gsub(/\.agda$/, ".html")
|
||||
html_path = File.join(["code", base_path, "html", html_file])
|
||||
|
||||
|
|
|
@ -1 +1 @@
|
|||
Subproject commit 3ccb5e8c65aab527f9fa72559db17ff7b07d042b
|
||||
Subproject commit 1aeb6007509f3e4e4b3f22207f752f2c7b6b2446
|
Loading…
Reference in New Issue
Block a user