diff -r 2677db44c795 -r 727ef1b8b3ee lib/Tools/display
--- a/lib/Tools/display	Wed Apr 13 09:48:41 2005 +0200
+++ b/lib/Tools/display	Wed Apr 13 18:34:22 2005 +0200
@@ -28,21 +28,6 @@
 }
 
 
-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
@@ -75,11 +60,22 @@
 
 [ -f "$FILE" ] || fail "Bad file: $FILE"
 
+case "$FILE" in
+    *.dvi)
+      VIEWER="$DVI_VIEWER"
+      ;;
+    *.pdf)
+      VIEWER="$PDF_VIEWER"
+      ;;
+    *)
+      fail "Unknown file type: $FILE";
+esac
+
 if [ -n "$CLEAN" ]; then
-  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE")
-  mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE"
-  view "$PRIVATE_FILE"
+  PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
+  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
+  $VIEWER "$PRIVATE_FILE"
   rm -f "$PRIVATE_FILE"
 else
-  view "$FILE"
+  exec $VIEWER "$FILE"
 fi