blob: 1620d2d7e9c9492f55cf48a08f39c81a315510f3 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
#!/bin/bash
tree -J ../theories -P "*.v" | jq --arg "current" "$1" -r '
("../" * ($current | [ scan("/+") ] | length)) as $prefix |
def make_item_link(prefix):
(if $current == prefix + .name then " class=\"current\"" else "" end) as $extra |
"<a href=\"\($prefix)\(prefix)\(.name | @uri).html\"\($extra)>\(.name | @html)</a>";
def handle_item(prefix):
if .type == "directory" then
"<li>\(.name | @html)<ul>" +
(.name as $dir | .contents | map(handle_item("\(prefix)\($dir)/")) | add) +
"</ul></li>"
else
"<li>\(make_item_link(prefix))</li>"
end;
.[0].contents | map(handle_item("")) | add
'
|
