eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
authorwenzelm
Sun, 25 Nov 2012 15:17:01 +0100
changeset 50197 b385d134926d
parent 50196 94886ebf090f
child 50198 0c7b351a6871
eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
etc/settings
lib/Tools/display
src/Doc/System/Basics.thy
--- a/etc/settings	Sat Nov 24 19:56:44 2012 +0100
+++ b/etc/settings	Sun Nov 25 15:17:01 2012 +0100
@@ -98,26 +98,26 @@
 # Preferred document format
 ISABELLE_DOC_FORMAT=pdf
 
-# The dvi file viewer
+# PDF file viewer (command-line to eval)
+case "$ISABELLE_PLATFORM_FAMILY" in
+  linux)
+    PDF_VIEWER="xdg-open"
+    ;;
+  macos)
+    PDF_VIEWER="open -W -n"
+    ;;
+  windows)
+    PDF_VIEWER="cygstart"
+    ;;
+esac
+
+# DVI file viewer (command-line to eval)
 DVI_VIEWER=xdvi
 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
 #DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7"
 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
-# The pdf file viewer
-case "$ISABELLE_PLATFORM" in
-  *-linux)
-    PDF_VIEWER="xdg-open"
-    ;;
-  *-darwin)
-    PDF_VIEWER="open -W -n"
-    ;;
-  *-cygwin)
-    PDF_VIEWER="cygstart"
-    ;;
-esac
-
 
 # Printer spool command for PS files
 PRINT_COMMAND=lp
--- a/lib/Tools/display	Sat Nov 24 19:56:44 2012 +0100
+++ b/lib/Tools/display	Sun Nov 25 15:17:01 2012 +0100
@@ -73,9 +73,9 @@
 if [ -n "$CLEAN" ]; then
   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
-  $VIEWER "$PRIVATE_FILE"
+  eval "$VIEWER \"$PRIVATE_FILE\""
   sleep 5   #try to avoid races
   rm -f "$PRIVATE_FILE"
 else
-  exec $VIEWER "$FILE"
+  eval "$VIEWER \"$FILE\""
 fi
--- a/src/Doc/System/Basics.thy	Sat Nov 24 19:56:44 2012 +0100
+++ b/src/Doc/System/Basics.thy	Sun Nov 25 15:17:01 2012 +0100
@@ -268,13 +268,13 @@
   directories with documentation files.
   
   \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
-  document format, typically @{verbatim dvi} or @{verbatim pdf}.
-  
-  \item[@{setting_def DVI_VIEWER}] specifies the command to be used
-  for displaying @{verbatim dvi} files.
-  
-  \item[@{setting_def PDF_VIEWER}] specifies the command to be used
-  for displaying @{verbatim pdf} files.
+  document format, typically @{verbatim pdf} or @{verbatim dvi}.
+
+  \item[@{setting_def PDF_VIEWER}] specifies the command-line to be
+  used for displaying @{verbatim pdf} files.
+
+  \item[@{setting_def DVI_VIEWER}] specifies the command-line to be
+  used for displaying @{verbatim dvi} files.
   
   \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
   spool command, which is expected to accept @{verbatim ps} files.