# 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