From 6203ffc9924ba8f14e127e4a5d6e451a637faedc Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 20 Jun 2019 10:58:02 +0200
Subject: [PATCH] Finished sed script for linking to the Agda stdlib

---
 .gitignore   |  1 +
 Makefile     |  2 ++
 highlight.sh | 35 ++++++++++++++++++++++++++++++++++-
 3 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index a1d1483d..59b6f31f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,6 +5,7 @@
 ## Jekyll files
 _site/
 .sass-cache/
+.agda-stdlib.sed
 .jekyll-metadata
 Gemfile.lock
 
diff --git a/Makefile b/Makefile
index 0c127321..32e8bee1 100644
--- a/Makefile
+++ b/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
diff --git a/highlight.sh b/highlight.sh
index b4010617..f00e6381 100755
--- a/highlight.sh
+++ b/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"