Initialize repository

1 files changed, 17 insertions, 0 deletions

diff --git a/explorer/tree.sh b/explorer/tree.sh
new file mode 100755
index 0000000..1620d2d
--- /dev/null
+++ b/explorer/tree.sh
@@ -0,0 +1,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
+'