lib/Tools/latex
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 9788 df671fa2562a
child 10511 efb3428c9879
permissions -rwxr-xr-x
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     1
#!/bin/bash
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     2
#
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 8568
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 8568
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     6
#
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
     7
# DESCRIPTION: run LaTeX (and related tools)
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     8
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     9
9788
wenzelm
parents: 8568
diff changeset
    10
PRG=$(basename "$0")
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    11
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    12
function usage()
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    13
{
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    14
  echo
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
    15
  echo "Usage: $PRG [OPTIONS] [FILE]"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    16
  echo
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    18
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    19
  echo "                 pdf, bbl, png, sty"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    20
  echo
7857
a49a3978fe3a tuned usage;
wenzelm
parents: 7815
diff changeset
    21
  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
a49a3978fe3a tuned usage;
wenzelm
parents: 7815
diff changeset
    22
  echo "  producing the specified output format."
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    23
  echo
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    24
  exit 1
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    25
}
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    26
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    27
function fail()
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    28
{
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    30
  exit 2
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    31
}
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    32
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    33
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    34
## process command line
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    35
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    36
# options
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    37
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    38
OUTFORMAT=dvi
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    39
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    40
while getopts "o:" OPT
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    41
do
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    42
  case "$OPT" in
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    43
    o)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    44
      OUTFORMAT="$OPTARG"
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    45
      ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    46
    \?)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    47
      usage
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    48
      ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    49
  esac
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    50
done
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    51
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    52
shift $(($OPTIND - 1))
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    53
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    54
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    55
# args
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    56
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
    57
FILE="root.tex"
9788
wenzelm
parents: 8568
diff changeset
    58
[ "$#" -ge 1 ] && { FILE="$1"; shift; }
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    59
9788
wenzelm
parents: 8568
diff changeset
    60
[ "$#" -ne 0 ] && usage
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    61
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    62
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    63
## main
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    64
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    65
# root file
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    66
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    67
DIR=$(dirname "$FILE")
9788
wenzelm
parents: 8568
diff changeset
    68
FILEBASE=$(basename "$FILE" .tex)
wenzelm
parents: 8568
diff changeset
    69
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    70
8568
wenzelm
parents: 8565
diff changeset
    71
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
    72
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    73
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    74
# operations
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    75
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    76
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    77
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    78
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    79
function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
7865
d9be8bc5624e support thumbpdf (via 'png' output format);
wenzelm
parents: 7857
diff changeset
    80
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    81
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    82
function update_styles ()
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    83
{
9788
wenzelm
parents: 8568
diff changeset
    84
  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    85
  do
8565
3c3895e37761 improved dump of styles;
wenzelm
parents: 8564
diff changeset
    86
    DEST="$DIR"/$(basename "$NAME")
3c3895e37761 improved dump of styles;
wenzelm
parents: 8564
diff changeset
    87
    if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
3c3895e37761 improved dump of styles;
wenzelm
parents: 8564
diff changeset
    88
      echo "updating $DEST"
3c3895e37761 improved dump of styles;
wenzelm
parents: 8564
diff changeset
    89
      cp -f "$NAME" "$DEST"
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    90
    fi
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    91
  done
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    92
}
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    93
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    94
case "$OUTFORMAT" in
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    95
  dvi)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    96
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    97
    run_latex
9788
wenzelm
parents: 8568
diff changeset
    98
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    99
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   100
  dvi.gz)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   101
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   102
    run_latex && \
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   103
    gzip -f "$FILEBASE.dvi"
9788
wenzelm
parents: 8568
diff changeset
   104
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   105
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   106
  ps)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   107
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   108
    run_latex && \
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   109
    run_dvips &&
9788
wenzelm
parents: 8568
diff changeset
   110
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   111
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   112
  ps.gz)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   113
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   114
    run_latex && \
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   115
    run_dvips &&
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   116
    gzip -f "$FILEBASE.ps"
9788
wenzelm
parents: 8568
diff changeset
   117
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   118
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   119
  pdf)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   120
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   121
    run_pdflatex
9788
wenzelm
parents: 8568
diff changeset
   122
    RC="$?"
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   123
    ;;
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   124
  bbl)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   125
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   126
    run_bibtex
9788
wenzelm
parents: 8568
diff changeset
   127
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   128
    ;;
7865
d9be8bc5624e support thumbpdf (via 'png' output format);
wenzelm
parents: 7857
diff changeset
   129
  png)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   130
    check_root && \
7865
d9be8bc5624e support thumbpdf (via 'png' output format);
wenzelm
parents: 7857
diff changeset
   131
    run_thumbpdf
9788
wenzelm
parents: 8568
diff changeset
   132
    RC="$?"
7865
d9be8bc5624e support thumbpdf (via 'png' output format);
wenzelm
parents: 7857
diff changeset
   133
    ;;
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   134
  sty)
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   135
    update_styles
9788
wenzelm
parents: 8568
diff changeset
   136
    RC="$?"
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   137
    ;;
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   138
  *)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   139
    fail "Bad output format '$OUTFORMAT'"
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   140
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   141
esac
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
   142
9788
wenzelm
parents: 8568
diff changeset
   143
exit "$RC"