display pdf as well as dvi
authorkleing
Thu Sep 30 07:14:34 2004 +0200 (2004-09-30)
changeset 1521839747a9e3c37
parent 15217 15fa818ef624
child 15219 fb4b5c2cca8b
display pdf as well as dvi
etc/settings
lib/Tools/display
     1.1 --- a/etc/settings	Thu Sep 30 05:08:17 2004 +0200
     1.2 +++ b/etc/settings	Thu Sep 30 07:14:34 2004 +0200
     1.3 @@ -152,6 +152,10 @@
     1.4  #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
     1.5  #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
     1.6  
     1.7 +#The pdf file viewer
     1.8 +PDF_VIEWER=acroread
     1.9 +#PDF_VIEWER=xpdf
    1.10 +
    1.11  #Printer spool command for PS files
    1.12  PRINT_COMMAND=lp
    1.13  
     2.1 --- a/lib/Tools/display	Thu Sep 30 05:08:17 2004 +0200
     2.2 +++ b/lib/Tools/display	Thu Sep 30 07:14:34 2004 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  # $Id$
     2.5  # Author: Markus Wenzel, TU Muenchen
     2.6  #
     2.7 -# DESCRIPTION: display document (in DVI format)
     2.8 +# DESCRIPTION: display document (in DVI or PDF format)
     2.9  
    2.10  
    2.11  PRG="$(basename "$0")"
    2.12 @@ -16,7 +16,7 @@
    2.13    echo "  Options are:"
    2.14    echo "    -c           cleanup -- remove FILE after use"
    2.15    echo
    2.16 -  echo "  Display document FILE (in DVI format)."
    2.17 +  echo "  Display document FILE (in DVI or PDF format)."
    2.18    echo
    2.19    exit 1
    2.20  }
    2.21 @@ -28,6 +28,21 @@
    2.22  }
    2.23  
    2.24  
    2.25 +function view()
    2.26 +{
    2.27 +  if [ "${1%%.dvi}.dvi" == "$1" ]; then
    2.28 +    exec $DVI_VIEWER "$1"
    2.29 +    return
    2.30 +  fi
    2.31 +
    2.32 +  if [ "${1%%.pdf}.pdf" == "$1" ]; then
    2.33 +    exec $PDF_VIEWER "$1"
    2.34 +    return
    2.35 +  fi
    2.36 +
    2.37 +  fail "Unknown file type: $FILE";
    2.38 +}
    2.39 +
    2.40  ## process command line
    2.41  
    2.42  # options
    2.43 @@ -61,10 +76,10 @@
    2.44  [ -f "$FILE" ] || fail "Bad file: $FILE"
    2.45  
    2.46  if [ -n "$CLEAN" ]; then
    2.47 -  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi
    2.48 +  PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE"
    2.49    mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    2.50 -  $DVI_VIEWER "$PRIVATE_FILE"
    2.51 +  view "$PRIVATE_FILE"
    2.52    rm -f "$PRIVATE_FILE"
    2.53  else
    2.54 -  exec $DVI_VIEWER "$FILE"
    2.55 +  view "$FILE"
    2.56  fi