lib/Tools/display

+#!/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=$(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