"isabelle logo" produces EPS and PDF format simultaneously;
more robust invocation of epstopdf: avoid filter mode;
--- 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
--- 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"
+
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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" .
--- 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.
--- 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" .
--- 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" .
--- 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" .