From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 explorer/tree.sh | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100755 explorer/tree.sh

(limited to 'explorer/tree.sh')

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
+'
-- 
cgit v1.2.3