diff -r 15fa818ef624 -r 39747a9e3c37 lib/Tools/display
--- a/lib/Tools/display	Thu Sep 30 05:08:17 2004 +0200
+++ b/lib/Tools/display	Thu Sep 30 07:14:34 2004 +0200
@@ -3,7 +3,7 @@
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 #
-# DESCRIPTION: display document (in DVI format)
+# DESCRIPTION: display document (in DVI or PDF format)
 
 
 PRG="$(basename "$0")"
@@ -16,7 +16,7 @@
   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
 }
@@ -28,6 +28,21 @@
 }
 
 
+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
@@ -61,10 +76,10 @@
 [ -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