# HG changeset patch
# User wenzelm
# Date 1601294030 -7200
# Node ID 3cc6aa40585848518cd005840a81c18fb93fc43a
# Parent  8162ca81ea8ad29bf087601fca20d934fd113061
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);

diff -r 8162ca81ea8a -r 3cc6aa405858 NEWS
--- a/NEWS	Sun Sep 27 23:02:25 2020 +0200
+++ b/NEWS	Mon Sep 28 13:53:50 2020 +0200
@@ -169,6 +169,10 @@
 * Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
 variable.
 
+* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
+(for DVI documents) has been discontinued. Former option -n has been
+turned into -o with explicit file name. Minor INCOMPATIBILITY.
+
 * The shell function "isabelle_directory" (within etc/settings of
 components) augments the list of special directories for persistent
 symbolic path names. This improves portability of heap images and
diff -r 8162ca81ea8a -r 3cc6aa405858 lib/Tools/logo
--- a/lib/Tools/logo	Sun Sep 27 23:02:25 2020 +0200
+++ b/lib/Tools/logo	Mon Sep 28 13:53:50 2020 +0200
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
 #
-# DESCRIPTION: create an instance of the Isabelle logo
+# DESCRIPTION: create an instance of the Isabelle logo (PDF)
 
 
 PRG="$(basename "$0")"
@@ -12,10 +12,10 @@
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
   echo
-  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
+  echo "  Create instance XYZ of the Isabelle logo (PDF)."
   echo
   echo "  Options are:"
-  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
+  echo "    -o FILE      alternative output file (default \"isabelle_xyx.pdf\")"
   echo "    -q           quiet mode"
   echo
   exit 1
@@ -32,14 +32,14 @@
 
 # options
 
-OUTPUT_NAME=""
+OUTPUT_FILE=""
 QUIET=""
 
-while getopts "n:q" OPT
+while getopts "o:q" OPT
 do
   case "$OPT" in
-    n)
-      OUTPUT_NAME="$OPTARG"
+    o)
+      OUTPUT_FILE="$OPTARG"
       ;;
     q)
       QUIET=true
@@ -63,25 +63,15 @@
 
 ## main
 
-case "$OUTPUT_NAME" in
-  "")
-    OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
-    if [ -z "$OUTPUT_NAME" ]; then
-      OUTPUT_NAME="isabelle"
-    else
-      OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
-    fi
-    ;;
-  */* | *.eps | *.pdf)
-    fail "Bad output base name: \"$OUTPUT_NAME\""
-    ;;
-  *)
-    ;;
-esac
+if [ -z "$OUTPUT_FILE" ]; then
+  OUTPUT_NAME="$(echo "$TEXT" | tr A-Z a-z)"
+  if [ -z "$OUTPUT_NAME" ]; then
+    OUTPUT_FILE="isabelle.pdf"
+  else
+    OUTPUT_FILE="isabelle_${OUTPUT_NAME}.pdf"
+  fi
+fi
 
-[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
-perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
-
-[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
-"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
-
+[ -z "$QUIET" ] && echo "$OUTPUT_FILE" >&2
+perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
+  "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE"
diff -r 8162ca81ea8a -r 3cc6aa405858 src/Doc/Sledgehammer/document/build
--- a/src/Doc/Sledgehammer/document/build	Sun Sep 27 23:02:25 2020 +0200
+++ b/src/Doc/Sledgehammer/document/build	Mon Sep 28 13:53:50 2020 +0200
@@ -5,6 +5,5 @@
 FORMAT="$1"
 VARIANT="$2"
 
-isabelle logo -n isabelle_sledgehammer "S/H"
+isabelle logo -o isabelle_sledgehammer.pdf "S/H"
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
-
diff -r 8162ca81ea8a -r 3cc6aa405858 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sun Sep 27 23:02:25 2020 +0200
+++ b/src/Doc/System/Misc.thy	Mon Sep 28 13:53:50 2020 +0200
@@ -321,21 +321,21 @@
 section \<open>Creating instances of the Isabelle logo\<close>
 
 text \<open>
-  The @{tool_def logo} tool creates instances of the generic Isabelle logo as
-  EPS and PDF, for inclusion in {\LaTeX} documents.
+  The @{tool_def logo} tool creates instances of the generic Isabelle logo,
+  for inclusion in PDF{\LaTeX} documents.
   @{verbatim [display]
-\<open>Usage: isabelle logo [OPTIONS] XYZ
+\<open>Usage: isabelle logo [OPTIONS] [XYZ]
 
-  Create instance XYZ of the Isabelle logo (as EPS and PDF).
+  Create instance XYZ of the Isabelle logo (PDF).
 
   Options are:
-    -n NAME      alternative output base name (default "isabelle_xyx")
+    -o FILE      alternative output file (default "isabelle_xyx.pdf")
     -q           quiet mode\<close>}
 
-  Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files.
-  The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case.
+  Option \<^verbatim>\<open>-o\<close> specifies an alternative output file: the default is
+  \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>\<^verbatim>\<open>.pdf\<close> (in lower-case).
 
-  Option \<^verbatim>\<open>-q\<close> omits printing of the result file name.
+  Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
 
   \<^medskip>
   Implementors of Isabelle tools and applications are encouraged to make