#!/usr/bin/env bash

#

# $Id$

# Author: Markus Wenzel, TU Muenchen

#

# DESCRIPTION: display document (in DVI or PDF format)

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

function usage()

{

  echo

  echo "Usage: isabelle $PRG [OPTIONS] FILE"

  echo

  echo "  Options are:"

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

  echo

  echo "  Display document FILE (in DVI or PDF 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"

case "$FILE" in

    *.dvi)

      VIEWER="$DVI_VIEWER"

      ;;

    *.pdf)

      VIEWER="$PDF_VIEWER"

      ;;

    *)

      fail "Unknown file type: $FILE";

esac

if [ -n "$CLEAN" ]; then

  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")

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

  $VIEWER "$PRIVATE_FILE"

  sleep 5   #try to avoid races

  rm -f "$PRIVATE_FILE"

else

  exec $VIEWER "$FILE"

fi