#!/bin/bash

# the twelf directory, must contain sudirectory bin
TWELFBIN=`dirname $0`

# configuration commands that are passed to Twelf before loading a file
CONFIG="set chatter 1\n"

# takes a list of file name arguments and checks the files, prints a report at the end
# if the first two arguments are -catalog URI, URI is used as the catalog server
# if the first two arguments are -omdoc DIR, all files are converted to OMDoc and stored in directory DIR
# otherwise the files are only checked

if [ $1 = -catalog ]; then 
  CONFIG="$CONFIG set catalog $2\n"; shift; shift
fi

if [ $1 = -unsafe ]; then 
  CONFIG="$CONFIG set unsafe true\n"; shift
fi

if [ $1 = -omdoc ]; then 
  TARGDIR="$2"; shift; shift
else
  TARGDIR=""
fi

# $ERROR counts the number of files with errors
ERROR=0
# $ERRORFILE collects error messages
ERRORFILE=""

# iterate over all files (must be relative paths?) that are passed via the command line
for file in $*
do
  # if requested, $COMMAND holds the command sent to Twelf for OMDoc conversion
  if [ "$TARGDIR" != '' ]; then
     # ".elf" is removed if present, ".omdoc" appended
     if [ "${file:0:1}" = "/" ]; then
       # if $file is absolute, only the base name is used
       NAME=`basename $file .elf`
       OFILE="$TARGDIR/$NAME.omdoc"
     else 
       # if $file is relative, it is appended to $TARGDIR
       OFILE="$TARGDIR/${file%\.elf}.omdoc"
     fi
     mkdir -p `dirname $OFILE`
     COMMAND="Print.OMDoc.printDoc $file $OFILE"
  else
    COMMAND=""
  fi

  # Twelf is called on the file with small verbosity, the output is printed and stored in $OUTPUT
  echo -e "\n*******************************"
  echo Processing $file
  OUTPUT=`echo -e "$CONFIG loadFile $file\n $COMMAND\n OS.exit" | $TWELFBIN/twelf-server`
  echo -e "$OUTPUT"

  # if there was an error ("ABORT" in the output), ...
  if echo -e "$OUTPUT" | grep "ABORT"; then
    # ... append error line to output that can be grepped for
    ERRORFILE="$ERRORFILE\n%% ERROR %% $file"
    # ... count errors
    ERROR=$(( $ERROR + 1))
    # ... if applicable, remove omdoc file (OMDoc conversion is called even after finding an error)
    if [ "$TARGDIR" != "" ]; then
      rm $OFILE
    fi
  fi
done

# If there were errors, print errors and number of errors
if [ $ERROR -gt 0 ]; then
  echo -e "\n*******************************"
  echo -e "$ERRORFILE"
  echo "There were $ERROR errors."
fi

# exit code is number of errors
exit $ERROR