"isabelle logo" produces EPS and PDF format simultaneously;
authorwenzelm
Mon Sep 03 11:09:25 2012 +0200 (2012-09-03)
changeset 49072747835eb2782
parent 49071 c1ca931b3647
child 49073 88fe93ae61cf
"isabelle logo" produces EPS and PDF format simultaneously;
more robust invocation of epstopdf: avoid filter mode;
NEWS
lib/Tools/logo
src/Doc/Classes/document/build
src/Doc/Codegen/document/build
src/Doc/HOL/document/build
src/Doc/Intro/document/build
src/Doc/IsarImplementation/document/build
src/Doc/IsarRef/document/build
src/Doc/Logics/document/build
src/Doc/Nitpick/document/build
src/Doc/ProgProve/document/build
src/Doc/Ref/document/build
src/Doc/Sledgehammer/document/build
src/Doc/System/Misc.thy
src/Doc/System/document/build
src/Doc/Tutorial/document/build
src/Doc/ZF/document/build
     1.1 --- a/NEWS	Mon Sep 03 10:17:17 2012 +0200
     1.2 +++ b/NEWS	Mon Sep 03 11:09:25 2012 +0200
     1.3 @@ -101,8 +101,8 @@
     1.4  picked up from some surrounding directory.  Potential INCOMPATIBILITY
     1.5  for home-made configurations.
     1.6  
     1.7 -* The "isabelle logo" tool allows to specify EPS or PDF format; the
     1.8 -latter is preferred now.  Minor INCOMPATIBILITY.
     1.9 +* The "isabelle logo" tool produces EPS and PDF format simultaneously.
    1.10 +Minor INCOMPATIBILITY in command-line options.
    1.11  
    1.12  * Advanced support for Isabelle sessions and build management, see
    1.13  "system" manual for the chapter of that name, especially the "isabelle
     2.1 --- a/lib/Tools/logo	Mon Sep 03 10:17:17 2012 +0200
     2.2 +++ b/lib/Tools/logo	Mon Sep 03 11:09:25 2012 +0200
     2.3 @@ -10,12 +10,12 @@
     2.4  function usage()
     2.5  {
     2.6    echo
     2.7 -  echo "Usage: isabelle $PRG [OPTIONS] NAME"
     2.8 +  echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
     2.9    echo
    2.10 -  echo "  Create instance NAME of the Isabelle logo (as EPS or PDF)."
    2.11 +  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
    2.12    echo
    2.13    echo "  Options are:"
    2.14 -  echo "    -o OUTPUT    specify output file and format (default \"isabelle_name.pdf\")"
    2.15 +  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
    2.16    echo "    -q           quiet mode"
    2.17    echo
    2.18    exit 1
    2.19 @@ -32,14 +32,14 @@
    2.20  
    2.21  # options
    2.22  
    2.23 -OUTPUT=""
    2.24 +OUTPUT_NAME=""
    2.25  QUIET=""
    2.26  
    2.27 -while getopts "o:q" OPT
    2.28 +while getopts "n:q" OPT
    2.29  do
    2.30    case "$OPT" in
    2.31 -    o)
    2.32 -      OUTPUT="$OPTARG"
    2.33 +    n)
    2.34 +      OUTPUT_NAME="$OPTARG"
    2.35        ;;
    2.36      q)
    2.37        QUIET=true
    2.38 @@ -55,38 +55,33 @@
    2.39  
    2.40  # args
    2.41  
    2.42 -NAME="-"
    2.43 -[ "$#" -ge 1 ] && { NAME="$1"; shift; }
    2.44 +TEXT=""
    2.45 +[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
    2.46  
    2.47 -[ "$#" -ne 0 -o "$NAME" = "-" ] && usage
    2.48 +[ "$#" -ne 0 ] && usage
    2.49  
    2.50  
    2.51  ## main
    2.52  
    2.53 -if [ -z "$OUTPUT" ]; then
    2.54 -  OUTPUT=$(echo "$NAME" | tr A-Z a-z)
    2.55 -  [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}"
    2.56 -  OUTPUT="isabelle${OUTPUT}.pdf"
    2.57 -  OUTPUT_FORMAT="pdf"
    2.58 -else
    2.59 -  case "$OUTPUT" in
    2.60 -    *.eps)
    2.61 -      OUTPUT_FORMAT="eps"
    2.62 -      ;;
    2.63 -    *.pdf)
    2.64 -      OUTPUT_FORMAT="pdf"
    2.65 -      ;;
    2.66 -    *)
    2.67 -      fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\""
    2.68 -      ;;
    2.69 -  esac
    2.70 -fi
    2.71 +case "$OUTPUT_NAME" in
    2.72 +  "")
    2.73 +    OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
    2.74 +    if [ -z "$OUTPUT_NAME" ]; then
    2.75 +      OUTPUT_NAME="isabelle"
    2.76 +    else
    2.77 +      OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
    2.78 +    fi
    2.79 +    ;;
    2.80 +  */* | *.eps | *.pdf)
    2.81 +    fail "Bad output base name: \"$OUTPUT_NAME\""
    2.82 +    ;;
    2.83 +  *)
    2.84 +    ;;
    2.85 +esac
    2.86  
    2.87 -[ -z "$QUIET" ] && echo "$OUTPUT" >&2
    2.88 +[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
    2.89 +perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
    2.90  
    2.91 -if [ "$OUTPUT_FORMAT" = "eps" ]; then
    2.92 -  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
    2.93 -else
    2.94 -  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
    2.95 -    "$ISABELLE_EPSTOPDF" -f > "$OUTPUT"
    2.96 -fi
    2.97 +[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
    2.98 +"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
    2.99 +
     3.1 --- a/src/Doc/Classes/document/build	Mon Sep 03 10:17:17 2012 +0200
     3.2 +++ b/src/Doc/Classes/document/build	Mon Sep 03 11:09:25 2012 +0200
     3.3 @@ -5,8 +5,7 @@
     3.4  FORMAT="$1"
     3.5  VARIANT="$2"
     3.6  
     3.7 -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
     3.8 -"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
     3.9 +"$ISABELLE_TOOL" logo Isar
    3.10  
    3.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    3.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     4.1 --- a/src/Doc/Codegen/document/build	Mon Sep 03 10:17:17 2012 +0200
     4.2 +++ b/src/Doc/Codegen/document/build	Mon Sep 03 11:09:25 2012 +0200
     4.3 @@ -5,8 +5,7 @@
     4.4  FORMAT="$1"
     4.5  VARIANT="$2"
     4.6  
     4.7 -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar"
     4.8 -"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar"
     4.9 +"$ISABELLE_TOOL" logo Isar
    4.10  
    4.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    4.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     5.1 --- a/src/Doc/HOL/document/build	Mon Sep 03 10:17:17 2012 +0200
     5.2 +++ b/src/Doc/HOL/document/build	Mon Sep 03 11:09:25 2012 +0200
     5.3 @@ -5,8 +5,7 @@
     5.4  FORMAT="$1"
     5.5  VARIANT="$2"
     5.6  
     5.7 -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
     5.8 -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
     5.9 +"$ISABELLE_TOOL" logo HOL
    5.10  
    5.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    5.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     6.1 --- a/src/Doc/Intro/document/build	Mon Sep 03 10:17:17 2012 +0200
     6.2 +++ b/src/Doc/Intro/document/build	Mon Sep 03 11:09:25 2012 +0200
     6.3 @@ -5,8 +5,7 @@
     6.4  FORMAT="$1"
     6.5  VARIANT="$2"
     6.6  
     6.7 -"$ISABELLE_TOOL" logo -o isabelle.pdf ""
     6.8 -"$ISABELLE_TOOL" logo -o isabelle.eps ""
     6.9 +"$ISABELLE_TOOL" logo
    6.10  
    6.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    6.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     7.1 --- a/src/Doc/IsarImplementation/document/build	Mon Sep 03 10:17:17 2012 +0200
     7.2 +++ b/src/Doc/IsarImplementation/document/build	Mon Sep 03 11:09:25 2012 +0200
     7.3 @@ -5,8 +5,7 @@
     7.4  FORMAT="$1"
     7.5  VARIANT="$2"
     7.6  
     7.7 -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
     7.8 -"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
     7.9 +"$ISABELLE_TOOL" logo Isar
    7.10  
    7.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    7.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     8.1 --- a/src/Doc/IsarRef/document/build	Mon Sep 03 10:17:17 2012 +0200
     8.2 +++ b/src/Doc/IsarRef/document/build	Mon Sep 03 11:09:25 2012 +0200
     8.3 @@ -5,8 +5,7 @@
     8.4  FORMAT="$1"
     8.5  VARIANT="$2"
     8.6  
     8.7 -"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar"
     8.8 -"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar"
     8.9 +"$ISABELLE_TOOL" logo Isar
    8.10  
    8.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    8.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     9.1 --- a/src/Doc/Logics/document/build	Mon Sep 03 10:17:17 2012 +0200
     9.2 +++ b/src/Doc/Logics/document/build	Mon Sep 03 11:09:25 2012 +0200
     9.3 @@ -5,8 +5,7 @@
     9.4  FORMAT="$1"
     9.5  VARIANT="$2"
     9.6  
     9.7 -"$ISABELLE_TOOL" logo -o isabelle.pdf ""
     9.8 -"$ISABELLE_TOOL" logo -o isabelle.eps ""
     9.9 +"$ISABELLE_TOOL" logo
    9.10  
    9.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    9.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
    10.1 --- a/src/Doc/Nitpick/document/build	Mon Sep 03 10:17:17 2012 +0200
    10.2 +++ b/src/Doc/Nitpick/document/build	Mon Sep 03 11:09:25 2012 +0200
    10.3 @@ -5,8 +5,7 @@
    10.4  FORMAT="$1"
    10.5  VARIANT="$2"
    10.6  
    10.7 -"$ISABELLE_TOOL" logo -o isabelle_nitpick.pdf "Nitpick"
    10.8 -"$ISABELLE_TOOL" logo -o isabelle_nitpick.eps "Nitpick"
    10.9 +"$ISABELLE_TOOL" logo Nitpick
   10.10  
   10.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
   10.12  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
    11.1 --- a/src/Doc/ProgProve/document/build	Mon Sep 03 10:17:17 2012 +0200
    11.2 +++ b/src/Doc/ProgProve/document/build	Mon Sep 03 11:09:25 2012 +0200
    11.3 @@ -5,8 +5,7 @@
    11.4  FORMAT="$1"
    11.5  VARIANT="$2"
    11.6  
    11.7 -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
    11.8 -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
    11.9 +"$ISABELLE_TOOL" logo HOL
   11.10  
   11.11  cp "$ISABELLE_HOME/src/Doc/ProgProve/MyList.thy" .
   11.12  
    12.1 --- a/src/Doc/Ref/document/build	Mon Sep 03 10:17:17 2012 +0200
    12.2 +++ b/src/Doc/Ref/document/build	Mon Sep 03 11:09:25 2012 +0200
    12.3 @@ -5,8 +5,7 @@
    12.4  FORMAT="$1"
    12.5  VARIANT="$2"
    12.6  
    12.7 -"$ISABELLE_TOOL" logo -o isabelle.pdf ""
    12.8 -"$ISABELLE_TOOL" logo -o isabelle.eps ""
    12.9 +"$ISABELLE_TOOL" logo
   12.10  
   12.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
   12.12  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
    13.1 --- a/src/Doc/Sledgehammer/document/build	Mon Sep 03 10:17:17 2012 +0200
    13.2 +++ b/src/Doc/Sledgehammer/document/build	Mon Sep 03 11:09:25 2012 +0200
    13.3 @@ -5,8 +5,7 @@
    13.4  FORMAT="$1"
    13.5  VARIANT="$2"
    13.6  
    13.7 -"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.pdf "S/H"
    13.8 -"$ISABELLE_TOOL" logo -o isabelle_sledgehammer.eps "S/H"
    13.9 +"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H"
   13.10  
   13.11  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
   13.12  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
    14.1 --- a/src/Doc/System/Misc.thy	Mon Sep 03 10:17:17 2012 +0200
    14.2 +++ b/src/Doc/System/Misc.thy	Mon Sep 03 11:09:25 2012 +0200
    14.3 @@ -209,23 +209,21 @@
    14.4  
    14.5  section {* Creating instances of the Isabelle logo *}
    14.6  
    14.7 -text {* The @{tool_def logo} tool creates any instance of the generic
    14.8 -  Isabelle logo as EPS or PDF.
    14.9 +text {* The @{tool_def logo} tool creates instances of the generic
   14.10 +  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
   14.11  \begin{ttbox}
   14.12 -Usage: isabelle logo [OPTIONS] NAME
   14.13 +Usage: isabelle logo [OPTIONS] XYZ
   14.14  
   14.15 -  Create instance NAME of the Isabelle logo (as EPS or PDF).
   14.16 +  Create instance XYZ of the Isabelle logo (as EPS and PDF).
   14.17  
   14.18    Options are:
   14.19 -    -o OUTFILE   specify output file and format
   14.20 -                 (default "isabelle_name.pdf")
   14.21 +    -n NAME      alternative output base name (default "isabelle_xyx")
   14.22      -q           quiet mode
   14.23  \end{ttbox}
   14.24  
   14.25 -  Option @{verbatim "-o"} specifies an explicit output file name and
   14.26 -  format, e.g.\ @{verbatim "mylogo.eps"} for an EPS logo.  The default
   14.27 -  is @{verbatim "isabelle_"}@{text name}@{verbatim ".pdf"}, with the
   14.28 -  lower-case version of the given name and PDF output.
   14.29 +  Option @{verbatim "-n"} specifies an altenative (base) name for the
   14.30 +  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
   14.31 +  in lower-case.
   14.32  
   14.33    Option @{verbatim "-q"} omits printing of the result file name.
   14.34  
    15.1 --- a/src/Doc/System/document/build	Mon Sep 03 10:17:17 2012 +0200
    15.2 +++ b/src/Doc/System/document/build	Mon Sep 03 11:09:25 2012 +0200
    15.3 @@ -5,8 +5,7 @@
    15.4  FORMAT="$1"
    15.5  VARIANT="$2"
    15.6  
    15.7 -"$ISABELLE_TOOL" logo -o isabelle.pdf ""
    15.8 -"$ISABELLE_TOOL" logo -o isabelle.eps ""
    15.9 +"$ISABELLE_TOOL" logo
   15.10  
   15.11  cp "$ISABELLE_HOME/src/Doc/IsarRef/document/style.sty" .
   15.12  cp "$ISABELLE_HOME/src/Doc/iman.sty" .
    16.1 --- a/src/Doc/Tutorial/document/build	Mon Sep 03 10:17:17 2012 +0200
    16.2 +++ b/src/Doc/Tutorial/document/build	Mon Sep 03 11:09:25 2012 +0200
    16.3 @@ -5,8 +5,7 @@
    16.4  FORMAT="$1"
    16.5  VARIANT="$2"
    16.6  
    16.7 -"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL"
    16.8 -"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL"
    16.9 +"$ISABELLE_TOOL" logo HOL
   16.10  
   16.11  cp "$ISABELLE_HOME/src/Doc/proof.sty" .
   16.12  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
    17.1 --- a/src/Doc/ZF/document/build	Mon Sep 03 10:17:17 2012 +0200
    17.2 +++ b/src/Doc/ZF/document/build	Mon Sep 03 11:09:25 2012 +0200
    17.3 @@ -5,8 +5,7 @@
    17.4  FORMAT="$1"
    17.5  VARIANT="$2"
    17.6  
    17.7 -"$ISABELLE_TOOL" logo -o isabelle_zf.pdf "ZF"
    17.8 -"$ISABELLE_TOOL" logo -o isabelle_zf.eps "ZF"
    17.9 +"$ISABELLE_TOOL" logo ZF
   17.10  
   17.11  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
   17.12  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .