# HG changeset patch
# User kleing
# Date 1096521274 -7200
# Node ID 39747a9e3c37c13e98a89fca3816136b802d4ba9
# Parent  15fa818ef6240439a7aac7929202e139145633c6
display pdf as well as dvi

diff -r 15fa818ef624 -r 39747a9e3c37 etc/settings
--- a/etc/settings	Thu Sep 30 05:08:17 2004 +0200
+++ b/etc/settings	Thu Sep 30 07:14:34 2004 +0200
@@ -152,6 +152,10 @@
 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
+#The pdf file viewer
+PDF_VIEWER=acroread
+#PDF_VIEWER=xpdf
+
 #Printer spool command for PS files
 PRINT_COMMAND=lp
 
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