Finished sed script for linking to the Agda stdlib

.gitignore

@@ -5,6 +5,7 @@
 ## Jekyll files
 _site/
 .sass-cache/
+.agda-stdlib.sed
 .jekyll-metadata
 Gemfile.lock
 

Makefile

@@ -4,6 +4,7 @@ agdai := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \)
 markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,,$(agda))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
+AGDA_STDLIB_SED := ".agda-stdlib.sed"
 
 ifeq ($(AGDA_STDLIB_VERSION),)
 AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/
@@ -73,6 +74,7 @@ build-incremental: $(markdown)
 
 # Remove all auxiliary files
 clean:
+	rm -f $(AGDA_STDLIB_SED)
 ifneq ($(strip $(agdai)),)
 	rm $(agdai)
 endif

highlight.sh

@@ -1,5 +1,7 @@
 #!/bin/bash
 
+AGDA_STDLIB_SED=".agda-stdlib.sed"
+
 SRC="$1"
 shift
 
@@ -7,19 +9,50 @@ OUT="$1"
 OUT_DIR="$(dirname $OUT)"
 shift
 
+# Create temporary directory and compute path to output of `agda --html`
 # NOTE: this assumes $OUT is equivalent to out/ plus the module path
 HTML_DIR="$(mktemp -d)"
 HTML="${OUT#out/}"
 HTML="/${HTML//\//.}"
 HTML="$HTML_DIR/$HTML"
 
+# Highlight Syntax using Agda
 set -o pipefail \
    && agda --html --html-highlight=code --html-dir="$HTML_DIR" "$SRC" "$@" \
     | sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$/d'
 
-sed -i "1 s|---|---\nsrc       : $SRC |" "$HTML"
+# Add source file to the Jekyll metadata
+sed -i "1 s|---|---\nsrc: $SRC|" "$HTML"
+
+# Add raw tags around Agda code blocks
 sed -i "s|<pre class=\"Agda\">|{% raw %}<pre class=\"Agda\">|" "$HTML"
 sed -i "s|</pre>|</pre>{% endraw %}|" "$HTML"
 
+# Fix links to the Agda standard library
+STDLIB_AGDALIB=`grep -m 1 "standard-library" $HOME/.agda/libraries`
+STDLIB_AGDALIB="$(eval "echo -e \"$STDLIB_AGDALIB\"")"
+
+STDLIB_INCLUDE=`grep -m 1 "include:" "$STDLIB_AGDALIB"`
+STDLIB_INCLUDE="${STDLIB_INCLUDE#include: }"
+
+STDLIB_PATH="$(dirname $STDLIB_AGDALIB)"
+STDLIB_PATH="$STDLIB_PATH/$STDLIB_INCLUDE"
+
+if [ -z "$AGDA_STDLIB_VERSION" ]; then
+    AGDA_STDLIB_URL="https://agda.github.io/agda-stdlib/"
+else
+    AGDA_STDLIB_URL="https://agda.github.io/agda-stdlib/v$AGDA_STDLIB_VERSION/"
+fi
+
+if [ ! -f "$AGDA_STDLIB_SED" ]; then
+    find "$STDLIB_PATH" -name "*.agda" -print0 | while read -d $'\0' AGDA_MODULE_PATH; do
+        AGDA_MODULE=$(eval "echo \"$AGDA_MODULE_PATH\" | sed -e \"s|$STDLIB_PATH/||g; s|/|\\\.|g; s|\.agda|\\\.html|g\"")
+        echo "s|$AGDA_MODULE|$AGDA_STDLIB_URL$AGDA_MODULE|g;" >> "$AGDA_STDLIB_SED"
+    done
+fi
+
+sed -i -f "$AGDA_STDLIB_SED" "$HTML"
+
+# Copy over the temporary file to the output path
 mkdir -p "$OUT_DIR"
 cp "$HTML" "$OUT"