lib/Tools/latex
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 52746 eec610972763
child 67263 449a989f42cd
permissions -rwxr-xr-x
updated for release;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: run LaTeX (and related tools)
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function 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, syms"
    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 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 OUTFORMAT=pdf
    36 
    37 while getopts "o:" OPT
    38 do
    39   case "$OPT" in
    40     o)
    41       OUTFORMAT="$OPTARG"
    42       ;;
    43     \?)
    44       usage
    45       ;;
    46   esac
    47 done
    48 
    49 shift $(($OPTIND - 1))
    50 
    51 
    52 # args
    53 
    54 FILE="root.tex"
    55 [ "$#" -ge 1 ] && { FILE="$1"; shift; }
    56 
    57 [ "$#" -ne 0 ] && usage
    58 
    59 
    60 ## main
    61 
    62 # root file
    63 
    64 DIR="$(dirname "$FILE")"
    65 FILEBASE="$(basename "$FILE" .tex)"
    66 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
    67 
    68 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
    69 
    70 
    71 # operations
    72 
    73 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    74 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    75 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    76 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    77 function 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 
    86 function extract_syms ()
    87 {
    88   perl -n \
    89     -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    90     "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
    91   perl -n \
    92     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    93     "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
    94 }
    95 
    96 case "$OUTFORMAT" in
    97   pdf)
    98     check_root && \
    99     run_pdflatex
   100     RC="$?"
   101     ;;
   102   dvi)
   103     check_root && \
   104     run_latex
   105     RC="$?"
   106     ;;
   107   bbl)
   108     check_root && \
   109     run_bibtex
   110     RC="$?"
   111     ;;
   112   idx)
   113     check_root && \
   114     run_makeindex
   115     RC="$?"
   116     ;;
   117   sty)
   118     copy_styles
   119     RC="$?"
   120     ;;
   121   syms)
   122     extract_syms
   123     RC="$?"
   124     ;;
   125   *)
   126     fail "Bad output format '$OUTFORMAT'"
   127     ;;
   128 esac
   129 
   130 exit "$RC"