# HG changeset patch # User wenzelm # Date 1353853021 -3600 # Node ID b385d134926d1b712fc8a90e16180668d3c5ed01 # Parent 94886ebf090f6a48701892c83020c0f382104b2f eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example; diff -r 94886ebf090f -r b385d134926d etc/settings --- 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 diff -r 94886ebf090f -r b385d134926d lib/Tools/display --- 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 diff -r 94886ebf090f -r b385d134926d src/Doc/System/Basics.thy --- 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.