1#!/usr/bin/env bash
2#
3# Author: Markus Wenzel, TU Muenchen
4#
5# DESCRIPTION: run LaTeX (and related tools)
6
7
8PRG="$(basename "$0")"
9
10function usage()
11{
12  echo
13  echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
14  echo
15  echo "  Options are:"
16  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty"
17  echo
18  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
19  echo "  producing the specified output format."
20  echo
21  exit 1
22}
23
24function fail()
25{
26  echo "$1" >&2
27  exit 2
28}
29
30
31## process command line
32
33# options
34
35OUTFORMAT=pdf
36
37while getopts "o:" OPT
38do
39  case "$OPT" in
40    o)
41      OUTFORMAT="$OPTARG"
42      ;;
43    \?)
44      usage
45      ;;
46  esac
47done
48
49shift $(($OPTIND - 1))
50
51
52# args
53
54FILE="root.tex"
55[ "$#" -ge 1 ] && { FILE="$1"; shift; }
56
57[ "$#" -ne 0 ] && usage
58
59
60## main
61
62# root file
63
64DIR="$(dirname "$FILE")"
65FILEBASE="$(basename "$FILE" .tex)"
66[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
67
68function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
69
70
71# operations
72
73function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
74function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
75function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
76function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
77function copy_styles ()
78{
79  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
80  do
81    TARGET="$DIR"/$(basename "$STYLEFILE")
82    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
83  done
84}
85
86case "$OUTFORMAT" in
87  pdf)
88    check_root && \
89    run_pdflatex
90    RC="$?"
91    ;;
92  dvi)
93    check_root && \
94    run_latex
95    RC="$?"
96    ;;
97  bbl)
98    check_root && \
99    run_bibtex
100    RC="$?"
101    ;;
102  idx)
103    check_root && \
104    run_makeindex
105    RC="$?"
106    ;;
107  sty)
108    copy_styles
109    RC="$?"
110    ;;
111  *)
112    fail "Bad output format '$OUTFORMAT'"
113    ;;
114esac
115
116exit "$RC"
117