#!/bin/bash

set -e

ARG="$1"

fail(){
	echo "$ARG: $*" >&2
	exit 1
}

exec < "$1"

read -r LINE || fail empty file

while :; do
	grep -q '^[^"]*\bimports\b' <<< "$LINE" && break
	read -r LINE || fail no imports
done

for THEORY in $(sed 's/^[^"]*\bimports\b *//' <<< "$LINE"); do
	if grep -q '^[A-Z]' <<< "$THEORY"; then
		if [ "$THEORY" = Pure ]; then
			continue
		fi

		FILE="$(dirname "$ARG")/$THEORY.thy"
	elif grep -q '^"~~/.*"$' <<< "$THEORY"; then
		FILE="/home/user/isabelle-2017/$(sed 's@^"~~/\(.*\)"$@\1@' <<< "$THEORY").thy"
	else
		fail "$THEORY" strange theory
	fi

	if ! [ -e "$FILE" ]; then
		fail "$FILE" problems with file
	fi

	echo "$FILE"
done

read -r LINE || fail eof after imports

while :; do
	if [ -n "$LINE" ]; then
		grep -q '^ *\(begin\|keywords\)\b' <<< "$LINE" && break
		fail begin expected but this found: "$LINE"
	fi

	read -r LINE || fail begin expected but eof found
done