clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;

--- a/NEWS	Fri Dec 06 21:49:08 2013 +0100
+++ b/NEWS	Fri Dec 06 22:10:45 2013 +0100
@@ -97,6 +97,19 @@
 formal context.
 
 
+*** System ***
+
+* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
+and PDF_VIEWER now refer to the actual programs, not shell
+command-lines.  Discontinued option -c: invocation may be asynchronous
+via desktop environment, without any special precautions.  Potential
+INCOMPATIBILITY with ambitious private settings.
+
+* Improved 'display_drafts' concerning desktop integration and
+repeated invocation in PIDE front-end: re-use single file
+$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
+
+
 
 New in Isabelle2013-2 (December 2013)
 -------------------------------------

--- a/etc/settings	Fri Dec 06 21:49:08 2013 +0100
+++ b/etc/settings	Fri Dec 06 22:10:45 2013 +0100
@@ -100,21 +100,21 @@
 # Where to look for docs (multiple dirs separated by ':').
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
-# PDF file viewer (command-line to eval)
+# PDF file viewer
 case "$ISABELLE_PLATFORM_FAMILY" in
   linux)
     PDF_VIEWER="xdg-open"
     ;;
   macos)
-    PDF_VIEWER="open -W -n -F"
+    PDF_VIEWER="open"
     ;;
   windows)
     PDF_VIEWER="cygstart"
     ;;
 esac
 
-# DVI file viewer (command-line to eval)
-DVI_VIEWER=xdvi
+# DVI file viewer
+DVI_VIEWER="xdvi"
 
 
 ###

--- a/lib/Tools/display	Fri Dec 06 21:49:08 2013 +0100
+++ b/lib/Tools/display	Fri Dec 06 22:10:45 2013 +0100
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 #
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
 #
 # DESCRIPTION: display document (in DVI or PDF format)
 
@@ -10,12 +10,9 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] FILE"
+  echo "Usage: isabelle $PRG DOCUMENT"
   echo
-  echo "  Options are:"
-  echo "    -c           cleanup -- remove FILE after use"
-  echo
-  echo "  Display document FILE (in DVI or PDF format)."
+  echo "  Display DOCUMENT (in DVI or PDF format)."
   echo
   exit 1
 }
@@ -27,55 +24,22 @@
 }
 
 
-## process command line
-
-# options
-
-CLEAN=""
-
-while getopts "c" OPT
-do
-  case "$OPT" in
-    c)
-      CLEAN=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 1 ] && usage
-
-FILE="$1"; shift
-
-
 ## main
 
-[ -f "$FILE" ] || fail "Bad file: $FILE"
+[ "$#" -ne 1 -o "$1" = "-?" ] && usage
+
+DOCUMENT="$1"; shift
+
+[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
 
-case "$FILE" in
-    *.dvi)
-      VIEWER="$DVI_VIEWER"
-      ;;
-    *.pdf)
-      VIEWER="$PDF_VIEWER"
-      ;;
-    *)
-      fail "Unknown file type: $FILE";
+case "$DOCUMENT" in
+  *.dvi)
+    exec "$DVI_VIEWER" "$DOCUMENT"
+    ;;
+  *.pdf)
+    exec "$PDF_VIEWER" "$DOCUMENT"
+    ;;
+  *)
+    fail "Unknown document type: \"$DOCUMENT\"";
 esac
 
-if [ -n "$CLEAN" ]; then
-  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
-  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
-  eval "$VIEWER \"$PRIVATE_FILE\""
-  sleep 5   #try to avoid races
-  rm -f "$PRIVATE_FILE"
-else
-  eval "$VIEWER \"$FILE\""
-fi

--- a/src/Doc/System/Basics.thy	Fri Dec 06 21:49:08 2013 +0100
+++ b/src/Doc/System/Basics.thy	Fri Dec 06 22:10:45 2013 +0100
@@ -267,12 +267,12 @@
   
   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   directories with documentation files.
-  
-  \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 PDF_VIEWER}] specifies the program to be used
+  for displaying @{verbatim pdf} files.
+
+  \item[@{setting_def DVI_VIEWER}] specifies the program to be used
+  for displaying @{verbatim dvi} files.
   
   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   prefix from which any running @{executable "isabelle-process"}

--- a/src/Doc/System/Misc.thy	Fri Dec 06 21:49:08 2013 +0100
+++ b/src/Doc/System/Misc.thy	Fri Dec 06 22:10:45 2013 +0100
@@ -65,20 +65,16 @@
 text {* The @{tool_def display} tool displays documents in DVI or PDF
   format:
 \begin{ttbox}
-Usage: isabelle display [OPTIONS] FILE
-
-  Options are:
-    -c           cleanup -- remove FILE after use
+Usage: isabelle display DOCUMENT
 
-  Display document FILE (in DVI or PDF format).
+  Display DOCUMENT (in DVI or PDF format).
 \end{ttbox}
 
-  \medskip The @{verbatim "-c"} option causes the input file to be
-  removed after use.
-
   \medskip The settings @{setting DVI_VIEWER} and @{setting
   PDF_VIEWER} determine the programs for viewing the corresponding
-  file formats.
+  file formats.  Normally this opens the document via the desktop
+  environment, potentially in an asynchronous manner with re-use of
+  previews views.
 *}
 
 

--- a/src/Pure/Thy/present.ML	Fri Dec 06 21:49:08 2013 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 06 22:10:45 2013 +0100
@@ -443,10 +443,13 @@
 
     val result =
       isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
-    val detachable_result = Isabelle_System.create_tmp_path documentN "pdf";
-    val _ = File.copy result detachable_result;
+
+    val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
+    val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
+    val _ = Isabelle_System.mkdirs target_dir;
+    val _ = File.copy result target;
   in
-    Isabelle_System.isabelle_tool "display" ("-c " ^ File.shell_path detachable_result ^ " &")
+    Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
   end);
 
 end;