#!/usr/bin/env bash

#

# $Id$

# Author: Markus Wenzel, TU Muenchen

# License: GPL (GNU GENERAL PUBLIC LICENSE)

#

# DESCRIPTION: display document (in DVI format)

PRG="$(basename "$0")"

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] FILE"

  echo

  echo "  Options are:"

  echo "    -c           cleanup -- remove FILE after use"

  echo

  echo "  Display document FILE (in DVI format)."

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

## process command line

# options

CLEAN=""

while getopts "c" OPT

do

  case "$OPT" in

    c)

      CLEAN=true

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

# args

[ "$#" -ne 1 ] && usage

FILE="$1"; shift

## main

[ -f "$FILE" ] || fail "Bad file: $FILE"

if [ -n "$CLEAN" ]; then

  PRIVATE_FILE=$ISABELLE_TMP/$(basename "$FILE" .dvi)$$.dvi

  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"

  $DVI_VIEWER "$PRIVATE_FILE"

  rm -f "$PRIVATE_FILE"

else

  exec $DVI_VIEWER "$FILE"

fi