lib/Tools/display

 #!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 #
-# DESCRIPTION: display document (in DVI format)
+# DESCRIPTION: display document (in DVI or PDF format)
 
 
 PRG="$(basename "$0")"
 
 function usage()

   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 "  Display document FILE (in DVI or PDF format)."
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
+
+function view()
+{
+  if [ "${1%%.dvi}.dvi" == "$1" ]; then
+    exec $DVI_VIEWER "$1"
+    return
+  fi
+
+  if [ "${1%%.pdf}.pdf" == "$1" ]; then
+    exec $PDF_VIEWER "$1"
+    return
+  fi
+
+  fail "Unknown file type: $FILE";
+}
 
 ## process command line
 
 # options
 

 ## main
 
 [ -f "$FILE" ] || fail "Bad file: $FILE"
 
 if [ -n "$CLEAN" ]; then
-  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi
+  PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE"
   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
-  $DVI_VIEWER "$PRIVATE_FILE"
+  view "$PRIVATE_FILE"
   rm -f "$PRIVATE_FILE"
 else
-  exec $DVI_VIEWER "$FILE"
+  view "$FILE"
 fi