lib/Tools/latex
author haftmann
Sun, 16 Oct 2016 09:31:04 +0200
changeset 64240 eabf80376aab
parent 52746 eec610972763
child 67263 449a989f42cd
permissions -rwxr-xr-x
more standardized names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     2
#
9788
wenzelm
parents: 8568
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     4
#
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
     5
# DESCRIPTION: run LaTeX (and related tools)
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     6
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     7
10511
wenzelm
parents: 9788
diff changeset
     8
PRG="$(basename "$0")"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
     9
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    10
function usage()
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    11
{
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 26979
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    14
  echo
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    15
  echo "  Options are:"
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
    16
  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty, syms"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    17
  echo
7857
a49a3978fe3a tuned usage;
wenzelm
parents: 7815
diff changeset
    18
  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
a49a3978fe3a tuned usage;
wenzelm
parents: 7815
diff changeset
    19
  echo "  producing the specified output format."
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    20
  echo
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    21
  exit 1
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    22
}
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    23
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    24
function fail()
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    25
{
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    27
  exit 2
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    28
}
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    29
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    30
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    31
## process command line
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    32
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    33
# options
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    34
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
    35
OUTFORMAT=pdf
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    36
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    37
while getopts "o:" OPT
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    38
do
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    39
  case "$OPT" in
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    40
    o)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    41
      OUTFORMAT="$OPTARG"
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    42
      ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    43
    \?)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    44
      usage
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    45
      ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    46
  esac
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    47
done
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    48
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    49
shift $(($OPTIND - 1))
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    50
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    51
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    52
# args
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    53
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
    54
FILE="root.tex"
9788
wenzelm
parents: 8568
diff changeset
    55
[ "$#" -ge 1 ] && { FILE="$1"; shift; }
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    56
9788
wenzelm
parents: 8568
diff changeset
    57
[ "$#" -ne 0 ] && usage
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    58
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    59
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    60
## main
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    61
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
    62
# root file
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    63
48515
3e17f343deb5 allow spaces in file names;
wenzelm
parents: 40893
diff changeset
    64
DIR="$(dirname "$FILE")"
3e17f343deb5 allow spaces in file names;
wenzelm
parents: 40893
diff changeset
    65
FILEBASE="$(basename "$FILE" .tex)"
9788
wenzelm
parents: 8568
diff changeset
    66
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    67
8568
wenzelm
parents: 8565
diff changeset
    68
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
    69
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    70
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    71
# operations
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    72
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    73
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    74
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    75
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
14344
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
    76
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
16064
7953879aa6cf ML_idf antiquotation
haftmann
parents: 15847
diff changeset
    77
function copy_styles ()
7953879aa6cf ML_idf antiquotation
haftmann
parents: 15847
diff changeset
    78
{
16161
519d717ae9e3 improved *.sty handling
haftmann
parents: 16064
diff changeset
    79
  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
519d717ae9e3 improved *.sty handling
haftmann
parents: 16064
diff changeset
    80
  do
16874
wenzelm
parents: 16171
diff changeset
    81
    TARGET="$DIR"/$(basename "$STYLEFILE")
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 16874
diff changeset
    82
    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
16161
519d717ae9e3 improved *.sty handling
haftmann
parents: 16064
diff changeset
    83
  done
16064
7953879aa6cf ML_idf antiquotation
haftmann
parents: 15847
diff changeset
    84
}
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
    85
14921
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    86
function extract_syms ()
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    87
{
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 16874
diff changeset
    88
  perl -n \
40893
7d88ebdce380 isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;
wenzelm
parents: 29143
diff changeset
    89
    -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
14921
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    90
    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 16874
diff changeset
    91
  perl -n \
14921
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    92
    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    93
    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    94
}
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
    95
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
    96
case "$OUTFORMAT" in
52746
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
    97
  pdf)
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
    98
    check_root && \
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
    99
    run_pdflatex
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
   100
    RC="$?"
eec610972763 discontinued historic document formats;
wenzelm
parents: 48515
diff changeset
   101
    ;;
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   102
  dvi)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   103
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   104
    run_latex
9788
wenzelm
parents: 8568
diff changeset
   105
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   106
    ;;
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   107
  bbl)
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   108
    check_root && \
7815
cd0fe98db185 support bibtex;
wenzelm
parents: 7794
diff changeset
   109
    run_bibtex
9788
wenzelm
parents: 8568
diff changeset
   110
    RC="$?"
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   111
    ;;
14344
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
   112
  idx)
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
   113
    check_root && \
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
   114
    run_makeindex
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
   115
    RC="$?"
0f0a2148a099 run makeindex if necessary
kleing
parents: 12846
diff changeset
   116
    ;;
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   117
  sty)
12846
0fce95478e19 copy_styles replaces overly conservative update_styles;
wenzelm
parents: 11845
diff changeset
   118
    copy_styles
9788
wenzelm
parents: 8568
diff changeset
   119
    RC="$?"
8564
37a1e855390a -o sty;
wenzelm
parents: 7865
diff changeset
   120
    ;;
14921
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
   121
  syms)
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
   122
    extract_syms
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
   123
    RC="$?"
4ad751fa50c1 added option 'isatool latex -o syms';
wenzelm
parents: 14344
diff changeset
   124
    ;;
7772
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   125
  *)
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   126
    fail "Bad output format '$OUTFORMAT'"
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   127
    ;;
c7b2f68c79fb Isabelle wrapper for LaTeX (and friends);
wenzelm
parents:
diff changeset
   128
esac
7794
37069d910cbe pass RC;
wenzelm
parents: 7777
diff changeset
   129
9788
wenzelm
parents: 8568
diff changeset
   130
exit "$RC"