lib/Tools/display
changeset 15218 39747a9e3c37
parent 15010 72fbe711e414
child 15223 e669fb5b0f5a
     1.1 --- a/lib/Tools/display	Thu Sep 30 05:08:17 2004 +0200
     1.2 +++ b/lib/Tools/display	Thu Sep 30 07:14:34 2004 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  # $Id$
     1.5  # Author: Markus Wenzel, TU Muenchen
     1.6  #
     1.7 -# DESCRIPTION: display document (in DVI format)
     1.8 +# DESCRIPTION: display document (in DVI or PDF format)
     1.9  
    1.10  
    1.11  PRG="$(basename "$0")"
    1.12 @@ -16,7 +16,7 @@
    1.13    echo "  Options are:"
    1.14    echo "    -c           cleanup -- remove FILE after use"
    1.15    echo
    1.16 -  echo "  Display document FILE (in DVI format)."
    1.17 +  echo "  Display document FILE (in DVI or PDF format)."
    1.18    echo
    1.19    exit 1
    1.20  }
    1.21 @@ -28,6 +28,21 @@
    1.22  }
    1.23  
    1.24  
    1.25 +function view()
    1.26 +{
    1.27 +  if [ "${1%%.dvi}.dvi" == "$1" ]; then
    1.28 +    exec $DVI_VIEWER "$1"
    1.29 +    return
    1.30 +  fi
    1.31 +
    1.32 +  if [ "${1%%.pdf}.pdf" == "$1" ]; then
    1.33 +    exec $PDF_VIEWER "$1"
    1.34 +    return
    1.35 +  fi
    1.36 +
    1.37 +  fail "Unknown file type: $FILE";
    1.38 +}
    1.39 +
    1.40  ## process command line
    1.41  
    1.42  # options
    1.43 @@ -61,10 +76,10 @@
    1.44  [ -f "$FILE" ] || fail "Bad file: $FILE"
    1.45  
    1.46  if [ -n "$CLEAN" ]; then
    1.47 -  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi
    1.48 +  PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE"
    1.49    mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    1.50 -  $DVI_VIEWER "$PRIVATE_FILE"
    1.51 +  view "$PRIVATE_FILE"
    1.52    rm -f "$PRIVATE_FILE"
    1.53  else
    1.54 -  exec $DVI_VIEWER "$FILE"
    1.55 +  view "$FILE"
    1.56  fi