# HG changeset patch
# User wenzelm
# Date 1346663365 -7200
# Node ID 747835eb2782a9bbc44f4294c82091b396514651
# Parent  c1ca931b36476ebf67be3e000df940f1c2f4b10d
"isabelle logo" produces EPS and PDF format simultaneously;
more robust invocation of epstopdf: avoid filter mode;

diff -r c1ca931b3647 -r 747835eb2782 NEWS
--- a/NEWS	Mon Sep 03 10:17:17 2012 +0200
+++ b/NEWS	Mon Sep 03 11:09:25 2012 +0200
@@ -101,8 +101,8 @@
 picked up from some surrounding directory.  Potential INCOMPATIBILITY
 for home-made configurations.
 
-* The "isabelle logo" tool allows to specify EPS or PDF format; the
-latter is preferred now.  Minor INCOMPATIBILITY.
+* The "isabelle logo" tool produces EPS and PDF format simultaneously.
+Minor INCOMPATIBILITY in command-line options.
 
 * Advanced support for Isabelle sessions and build management, see
 "system" manual for the chapter of that name, especially the "isabelle
diff -r c1ca931b3647 -r 747835eb2782 lib/Tools/logo
--- a/lib/Tools/logo	Mon Sep 03 10:17:17 2012 +0200
+++ b/lib/Tools/logo	Mon Sep 03 11:09:25 2012 +0200
@@ -10,12 +10,12 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] NAME"
+  echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
   echo
-  echo "  Create instance NAME of the Isabelle logo (as EPS or PDF)."
+  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
   echo
   echo "  Options are:"
-  echo "    -o OUTPUT    specify output file and format (default \"isabelle_name.pdf\")"
+  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
   echo "    -q           quiet mode"
   echo
   exit 1
@@ -32,14 +32,14 @@
 
 # options
 
-OUTPUT=""
+OUTPUT_NAME=""
 QUIET=""
 
-while getopts "o:q" OPT
+while getopts "n:q" OPT
 do
   case "$OPT" in
-    o)
-      OUTPUT="$OPTARG"
+    n)
+      OUTPUT_NAME="$OPTARG"
       ;;
     q)
       QUIET=true
@@ -55,38 +55,33 @@
 
 # args
 
-NAME="-"
-[ "$#" -ge 1 ] && { NAME="$1"; shift; }
+TEXT=""
+[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
 
-[ "$#" -ne 0 -o "$NAME" = "-" ] && usage
+[ "$#" -ne 0 ] && usage
 
 
 ## main
 
-if [ -z "$OUTPUT" ]; then
-  OUTPUT=$(echo "$NAME" | tr A-Z a-z)
-  [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}"
-  OUTPUT="isabelle${OUTPUT}.pdf"
-  OUTPUT_FORMAT="pdf"
-else
-  case "$OUTPUT" in
-    *.eps)
-      OUTPUT_FORMAT="eps"
-      ;;
-    *.pdf)
-      OUTPUT_FORMAT="pdf"
-      ;;
-    *)
-      fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\""
-      ;;
-  esac
-fi
+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
 
-[ -z "$QUIET" ] && echo "$OUTPUT" >&2
+[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
+perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
 
-if [ "$OUTPUT_FORMAT" = "eps" ]; then
-  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
-else
-  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
-    "$ISABELLE_EPSTOPDF" -f > "$OUTPUT"
-fi
+[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
+"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
+
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Classes/document/build
--- a/src/Doc/Classes/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Classes/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
+"$ISABELLE_TOOL" logo Isar
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Codegen/document/build
--- a/src/Doc/Codegen/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Codegen/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar"
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar"
+"$ISABELLE_TOOL" logo Isar
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/HOL/document/build
--- a/src/Doc/HOL/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/HOL/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
-"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
+"$ISABELLE_TOOL" logo HOL
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Intro/document/build
--- a/src/Doc/Intro/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Intro/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle.pdf ""
-"$ISABELLE_TOOL" logo -o isabelle.eps ""
+"$ISABELLE_TOOL" logo
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/IsarImplementation/document/build
--- a/src/Doc/IsarImplementation/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/IsarImplementation/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
+"$ISABELLE_TOOL" logo Isar
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/IsarRef/document/build
--- a/src/Doc/IsarRef/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/IsarRef/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar"
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar"
+"$ISABELLE_TOOL" logo Isar
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Logics/document/build
--- a/src/Doc/Logics/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Logics/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle.pdf ""
-"$ISABELLE_TOOL" logo -o isabelle.eps ""
+"$ISABELLE_TOOL" logo
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Nitpick/document/build
--- a/src/Doc/Nitpick/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Nitpick/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_nitpick.pdf "Nitpick"
-"$ISABELLE_TOOL" logo -o isabelle_nitpick.eps "Nitpick"
+"$ISABELLE_TOOL" logo Nitpick
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/manual.bib" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/ProgProve/document/build
--- a/src/Doc/ProgProve/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/ProgProve/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
-"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
+"$ISABELLE_TOOL" logo HOL
 
 cp "$ISABELLE_HOME/src/Doc/ProgProve/MyList.thy" .
 
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Ref/document/build
--- a/src/Doc/Ref/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Ref/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle.pdf ""
-"$ISABELLE_TOOL" logo -o isabelle.eps ""
+"$ISABELLE_TOOL" logo
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/extra.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Sledgehammer/document/build
--- a/src/Doc/Sledgehammer/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Sledgehammer/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.pdf "S/H"
-"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.eps "S/H"
+"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H"
 
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
 cp "$ISABELLE_HOME/src/Doc/manual.bib" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/System/Misc.thy	Mon Sep 03 11:09:25 2012 +0200
@@ -209,23 +209,21 @@
 
 section {* Creating instances of the Isabelle logo *}
 
-text {* The @{tool_def logo} tool creates any instance of the generic
-  Isabelle logo as EPS or PDF.
+text {* The @{tool_def logo} tool creates instances of the generic
+  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
 \begin{ttbox}
-Usage: isabelle logo [OPTIONS] NAME
+Usage: isabelle logo [OPTIONS] XYZ
 
-  Create instance NAME of the Isabelle logo (as EPS or PDF).
+  Create instance XYZ of the Isabelle logo (as EPS and PDF).
 
   Options are:
-    -o OUTFILE   specify output file and format
-                 (default "isabelle_name.pdf")
+    -n NAME      alternative output base name (default "isabelle_xyx")
     -q           quiet mode
 \end{ttbox}
 
-  Option @{verbatim "-o"} specifies an explicit output file name and
-  format, e.g.\ @{verbatim "mylogo.eps"} for an EPS logo.  The default
-  is @{verbatim "isabelle_"}@{text name}@{verbatim ".pdf"}, with the
-  lower-case version of the given name and PDF output.
+  Option @{verbatim "-n"} specifies an altenative (base) name for the
+  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
+  in lower-case.
 
   Option @{verbatim "-q"} omits printing of the result file name.
 
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/System/document/build
--- a/src/Doc/System/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/System/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle.pdf ""
-"$ISABELLE_TOOL" logo -o isabelle.eps ""
+"$ISABELLE_TOOL" logo
 
 cp "$ISABELLE_HOME/src/Doc/IsarRef/document/style.sty" .
 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/Tutorial/document/build
--- a/src/Doc/Tutorial/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/Tutorial/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
-"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
+"$ISABELLE_TOOL" logo HOL
 
 cp "$ISABELLE_HOME/src/Doc/proof.sty" .
 cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
diff -r c1ca931b3647 -r 747835eb2782 src/Doc/ZF/document/build
--- a/src/Doc/ZF/document/build	Mon Sep 03 10:17:17 2012 +0200
+++ b/src/Doc/ZF/document/build	Mon Sep 03 11:09:25 2012 +0200
@@ -5,8 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -o isabelle_zf.pdf "ZF"
-"$ISABELLE_TOOL" logo -o isabelle_zf.eps "ZF"
+"$ISABELLE_TOOL" logo ZF
 
 cp "$ISABELLE_HOME/src/Doc/isar.sty" .
 cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .