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