From 7eea42d37077b31c1fa11d900be54fbc00b52b59 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Tue, 10 Mar 2020 17:39:00 +0000
Subject: [PATCH] Minor changes in highlight script.
---
highlight.sh | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/highlight.sh b/highlight.sh
index 3a73100d..e6caefb9 100755
--- a/highlight.sh
+++ b/highlight.sh
@@ -23,9 +23,18 @@ function html_path {
HTML_DIR="$2"
# Extract the module name from the Agda file
- # NOTE: this fails if there is more than a single space after 'module'
+ #
+ # NOTE: This fails when there is no module statement,
+ # or when there is more than one space after 'module'.
+ #
MOD_NAME=`grep -o -m 1 "module\\s*\\(\\S\\S*\\)\\s.*where$" "$SRC" | cut -d ' ' -f 2`
+ if [ -z "$MOD_NAME" ]
+ then
+ echo "Error: No module header detected in '$SRC'" 1>&2
+ exit 1
+ fi
+
# Extract the extension from the Agda file
SRC_EXT="$(basename $SRC)"
SRC_EXT="${SRC_EXT##*.}"
@@ -44,7 +53,7 @@ set -o pipefail \
# Check if the highlighted file was successfully generated
if [[ ! -f "$HTML" ]]; then
- echo "File not generated: $FILE"
+ echo "Error: File not generated: '$FILE'" 1>&2
exit 1
fi