michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Minor changes in highlight script.

Browse source
This commit is contained in:
Wen Kokke 2020-03-10 17:39:00 +00:00
parent 5bfc503eec
commit 7eea42d370
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
highlight.sh
View file

@ -23,9 +23,18 @@ function html_path {
HTML_DIR="$2" HTML_DIR="$2"
# Extract the module name from the Agda file # 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` 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 # Extract the extension from the Agda file
SRC_EXT="$(basename $SRC)" SRC_EXT="$(basename $SRC)"
SRC_EXT="${SRC_EXT##*.}" SRC_EXT="${SRC_EXT##*.}"
@ -44,7 +53,7 @@ set -o pipefail \
# Check if the highlighted file was successfully generated # Check if the highlighted file was successfully generated
if [[ ! -f "$HTML" ]]; then if [[ ! -f "$HTML" ]]; then
echo "File not generated: $FILE" echo "Error: File not generated: '$FILE'" 1>&2
exit 1 exit 1
fi fi