#!/usr/bin/env bash

 #

 # 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"

   rm -f "$PRIVATE_FILE"

 else

   exec $VIEWER "$FILE"

 fi