# HG changeset patch
# User wenzelm
# Date 1346076654 -7200
# Node ID e6d9e46ff7bcb181ca693541f3f19851923949c4
# Parent  4c92a2f310b6ad8daf9f107f60ebea0b041a59be
clarified "isabelle logo";

diff -r 4c92a2f310b6 -r e6d9e46ff7bc NEWS
--- a/NEWS	Mon Aug 27 16:07:48 2012 +0200
+++ b/NEWS	Mon Aug 27 16:10:54 2012 +0200
@@ -84,6 +84,9 @@
 
 *** System ***
 
+* The "isabelle logo" tool allows to specify EPS or PDF format; the
+latter is preferred now.  Minor INCOMPATIBILITY.
+
 * Advanced support for Isabelle sessions and build management, see
 "system" manual for the chapter of that name, especially the "isabelle
 build" tool and its examples.  INCOMPATIBILITY, isabelle usedir /
diff -r 4c92a2f310b6 -r e6d9e46ff7bc doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Mon Aug 27 16:07:48 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy	Mon Aug 27 16:10:54 2012 +0200
@@ -210,19 +210,28 @@
 section {* Creating instances of the Isabelle logo *}
 
 text {* The @{tool_def logo} tool creates any instance of the generic
-  Isabelle logo as an Encapsuled Postscript file (EPS):
+  Isabelle logo as EPS or PDF.
 \begin{ttbox}
 Usage: isabelle logo [OPTIONS] NAME
 
-  Create instance NAME of the Isabelle logo (as EPS).
+  Create instance NAME of the Isabelle logo (as EPS or PDF).
 
   Options are:
-    -o OUTFILE   set output file (default determined from NAME)
+    -o OUTFILE   specify output file and format
+                 (default "isabelle_name.pdf")
     -q           quiet mode
 \end{ttbox}
-  You are encouraged to use this to create a derived logo for your
-  Isabelle project.  For example, @{tool logo}~@{verbatim Bali}
-  creates @{verbatim isabelle_bali.eps}.  *}
+
+  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 "-q"} omits printing of the result file name.
+
+  \medskip Implementors of Isabelle tools and applications are
+  encouraged to make derived Isabelle logos for their own projects
+  using this template.  *}
 
 
 section {* Isabelle wrapper for make \label{sec:tool-make} *}
diff -r 4c92a2f310b6 -r e6d9e46ff7bc doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Mon Aug 27 16:07:48 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex	Mon Aug 27 16:10:54 2012 +0200
@@ -250,19 +250,28 @@
 %
 \begin{isamarkuptext}%
 The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}} tool creates any instance of the generic
-  Isabelle logo as an Encapsuled Postscript file (EPS):
+  Isabelle logo as EPS or PDF.
 \begin{ttbox}
 Usage: isabelle logo [OPTIONS] NAME
 
-  Create instance NAME of the Isabelle logo (as EPS).
+  Create instance NAME of the Isabelle logo (as EPS or PDF).
 
   Options are:
-    -o OUTFILE   set output file (default determined from NAME)
+    -o OUTFILE   specify output file and format
+                 (default "isabelle_name.pdf")
     -q           quiet mode
 \end{ttbox}
-  You are encouraged to use this to create a derived logo for your
-  Isabelle project.  For example, \hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}~\verb|Bali|
-  creates \verb|isabelle_bali.eps|.%
+
+  Option \verb|-o| specifies an explicit output file name and
+  format, e.g.\ \verb|mylogo.eps| for an EPS logo.  The default
+  is \verb|isabelle_|\isa{name}\verb|.pdf|, with the
+  lower-case version of the given name and PDF output.
+
+  Option \verb|-q| omits printing of the result file name.
+
+  \medskip Implementors of Isabelle tools and applications are
+  encouraged to make derived Isabelle logos for their own projects
+  using this template.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 4c92a2f310b6 -r e6d9e46ff7bc lib/Tools/logo
--- a/lib/Tools/logo	Mon Aug 27 16:07:48 2012 +0200
+++ b/lib/Tools/logo	Mon Aug 27 16:10:54 2012 +0200
@@ -12,10 +12,10 @@
   echo
   echo "Usage: isabelle $PRG [OPTIONS] NAME"
   echo
-  echo "  Create instance NAME of the Isabelle logo (as EPS)."
+  echo "  Create instance NAME of the Isabelle logo (as EPS or PDF)."
   echo
   echo "  Options are:"
-  echo "    -o OUTFILE   set output file (default determined from NAME)"
+  echo "    -o OUTPUT    specify output file and format (default \"isabelle_name.pdf\")"
   echo "    -q           quiet mode"
   echo
   exit 1
@@ -32,14 +32,14 @@
 
 # options
 
-OUTFILE=""
+OUTPUT=""
 QUIET=""
 
 while getopts "o:q" OPT
 do
   case "$OPT" in
     o)
-      OUTFILE="$OPTARG"
+      OUTPUT="$OPTARG"
       ;;
     q)
       QUIET=true
@@ -63,15 +63,30 @@
 
 ## main
 
-if [ -z "$OUTFILE" ]; then
-  OUTFILE=$(echo "$NAME" | tr A-Z a-z)
-  [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
-  OUTFILE="isabelle${OUTFILE}.eps"
+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
 
-if [ "$OUTFILE" = "-" ]; then
-  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
+[ -z "$QUIET" ] && echo "$OUTPUT" >&2
+
+if [ "$OUTPUT_FORMAT" = "eps" ]; then
+  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
 else
-  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
-  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
+  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
+    "$ISABELLE_EPSTOPDF" -f > "$OUTPUT"
 fi