#!/bin/bash

set -e

failuremsg="Error"
failurecode=1

while [ $# -gt 0 ]
do
    case "$1" in
        --warning|-w)
            failuremsg="Warning"
            failurecode=0;;
    esac
    shift
done

echo "Checking for theories that are not part of an Isabelle session:"
echo "==============================================================="

PWD=`pwd`
TMPDIR=`mktemp -d`
isabelle build  -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
thylist=`comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt`
if [ -z "$thylist" ] ; then
    echo "  * Success: No dangling theories found."
    exit 0
else
    echo -e "$thylist"
    echo "$failuremsg: Dangling theories found (see list above)!" 
    exit $failurecode 
fi