--- 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 /
--- 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} *}
--- 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%
%
--- 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