lib/Tools/latex
author haftmann
Wed Jun 01 14:16:45 2005 +0200 (2005-06-01)
changeset 16170 75cb95f4825f
parent 16163 a9f460f16fd6
child 16171 3c939bb52420
permissions -rwxr-xr-x
remove CVS id from *.sty latex styles
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@7772
     2
#
wenzelm@7772
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@7772
     5
#
wenzelm@7794
     6
# DESCRIPTION: run LaTeX (and related tools)
wenzelm@7772
     7
wenzelm@7772
     8
wenzelm@10511
     9
PRG="$(basename "$0")"
wenzelm@7772
    10
wenzelm@7772
    11
function usage()
wenzelm@7772
    12
{
wenzelm@7772
    13
  echo
wenzelm@7794
    14
  echo "Usage: $PRG [OPTIONS] [FILE]"
wenzelm@7772
    15
  echo
wenzelm@7772
    16
  echo "  Options are:"
wenzelm@7815
    17
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
wenzelm@14921
    18
  echo "                 pdf, bbl, png, sty, syms"
wenzelm@7772
    19
  echo
wenzelm@7857
    20
  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
wenzelm@7857
    21
  echo "  producing the specified output format."
wenzelm@7772
    22
  echo
wenzelm@7772
    23
  exit 1
wenzelm@7772
    24
}
wenzelm@7772
    25
wenzelm@7772
    26
function fail()
wenzelm@7772
    27
{
wenzelm@7772
    28
  echo "$1" >&2
wenzelm@7772
    29
  exit 2
wenzelm@7772
    30
}
wenzelm@7772
    31
wenzelm@7772
    32
wenzelm@7772
    33
## process command line
wenzelm@7772
    34
wenzelm@7772
    35
# options
wenzelm@7772
    36
wenzelm@7772
    37
OUTFORMAT=dvi
wenzelm@7772
    38
wenzelm@7772
    39
while getopts "o:" OPT
wenzelm@7772
    40
do
wenzelm@7772
    41
  case "$OPT" in
wenzelm@7772
    42
    o)
wenzelm@7772
    43
      OUTFORMAT="$OPTARG"
wenzelm@7772
    44
      ;;
wenzelm@7772
    45
    \?)
wenzelm@7772
    46
      usage
wenzelm@7772
    47
      ;;
wenzelm@7772
    48
  esac
wenzelm@7772
    49
done
wenzelm@7772
    50
wenzelm@7772
    51
shift $(($OPTIND - 1))
wenzelm@7772
    52
wenzelm@7772
    53
wenzelm@7772
    54
# args
wenzelm@7772
    55
wenzelm@7794
    56
FILE="root.tex"
wenzelm@9788
    57
[ "$#" -ge 1 ] && { FILE="$1"; shift; }
wenzelm@7772
    58
wenzelm@9788
    59
[ "$#" -ne 0 ] && usage
wenzelm@7772
    60
wenzelm@7772
    61
wenzelm@7772
    62
## main
wenzelm@7772
    63
wenzelm@8564
    64
# root file
wenzelm@7815
    65
wenzelm@7772
    66
DIR=$(dirname "$FILE")
wenzelm@9788
    67
FILEBASE=$(basename "$FILE" .tex)
wenzelm@9788
    68
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
wenzelm@7772
    69
wenzelm@8568
    70
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
wenzelm@7794
    71
wenzelm@7815
    72
wenzelm@7815
    73
# operations
wenzelm@7815
    74
wenzelm@14921
    75
#set by configure
wenzelm@15847
    76
AUTO_PERL=perl
wenzelm@14921
    77
wenzelm@7815
    78
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    79
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    80
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
kleing@14344
    81
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
wenzelm@11845
    82
function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
wenzelm@7865
    83
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
haftmann@16064
    84
function copy_styles ()
haftmann@16064
    85
{
haftmann@16161
    86
  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
haftmann@16161
    87
  do
haftmann@16161
    88
    TARGET="$DIR"/$(basename $STYLEFILE)
haftmann@16161
    89
    rm -f $TARGET
haftmann@16170
    90
    "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g; print;' "$STYLEFILE" > "$TARGET"
haftmann@16170
    91
    #~ "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET
haftmann@16170
    92
    #~ # the [I] is there to prevent CVS from expanding $Id...$ itself ;-)
haftmann@16161
    93
  done
haftmann@16064
    94
}
wenzelm@7815
    95
wenzelm@14921
    96
function extract_syms ()
wenzelm@14921
    97
{
wenzelm@14921
    98
  "$AUTO_PERL" -n \
wenzelm@14970
    99
    -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
wenzelm@14921
   100
    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
wenzelm@14921
   101
  "$AUTO_PERL" -n \
wenzelm@14921
   102
    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
wenzelm@14921
   103
    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
wenzelm@14921
   104
}
wenzelm@14921
   105
wenzelm@7772
   106
case "$OUTFORMAT" in
wenzelm@7772
   107
  dvi)
wenzelm@8564
   108
    check_root && \
wenzelm@7815
   109
    run_latex
wenzelm@9788
   110
    RC="$?"
wenzelm@7772
   111
    ;;
wenzelm@7772
   112
  dvi.gz)
wenzelm@8564
   113
    check_root && \
wenzelm@7815
   114
    run_latex && \
wenzelm@7772
   115
    gzip -f "$FILEBASE.dvi"
wenzelm@9788
   116
    RC="$?"
wenzelm@7772
   117
    ;;
wenzelm@7772
   118
  ps)
wenzelm@8564
   119
    check_root && \
wenzelm@7815
   120
    run_latex && \
wenzelm@7815
   121
    run_dvips &&
wenzelm@9788
   122
    RC="$?"
wenzelm@7772
   123
    ;;
wenzelm@7772
   124
  ps.gz)
wenzelm@8564
   125
    check_root && \
wenzelm@7815
   126
    run_latex && \
wenzelm@7815
   127
    run_dvips &&
wenzelm@7772
   128
    gzip -f "$FILEBASE.ps"
wenzelm@9788
   129
    RC="$?"
wenzelm@7772
   130
    ;;
wenzelm@7772
   131
  pdf)
wenzelm@8564
   132
    check_root && \
wenzelm@7815
   133
    run_pdflatex
wenzelm@9788
   134
    RC="$?"
wenzelm@7815
   135
    ;;
wenzelm@7815
   136
  bbl)
wenzelm@8564
   137
    check_root && \
wenzelm@7815
   138
    run_bibtex
wenzelm@9788
   139
    RC="$?"
wenzelm@7772
   140
    ;;
kleing@14344
   141
  idx)
kleing@14344
   142
    check_root && \
kleing@14344
   143
    run_makeindex
kleing@14344
   144
    RC="$?"
kleing@14344
   145
    ;;
wenzelm@7865
   146
  png)
wenzelm@8564
   147
    check_root && \
wenzelm@7865
   148
    run_thumbpdf
wenzelm@9788
   149
    RC="$?"
wenzelm@7865
   150
    ;;
wenzelm@8564
   151
  sty)
wenzelm@12846
   152
    copy_styles
wenzelm@9788
   153
    RC="$?"
wenzelm@8564
   154
    ;;
wenzelm@14921
   155
  syms)
wenzelm@14921
   156
    extract_syms
wenzelm@14921
   157
    RC="$?"
wenzelm@14921
   158
    ;;
wenzelm@7772
   159
  *)
wenzelm@7772
   160
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7772
   161
    ;;
wenzelm@7772
   162
esac
wenzelm@7794
   163
wenzelm@9788
   164
exit "$RC"