lib/Tools/latex
author wenzelm
Fri Dec 22 18:32:59 2017 +0100 (2017-12-22 ago)
changeset 67264 449a989f42cd
parent 52746 eec610972763
permissions -rwxr-xr-x
discontinued 'display_drafts' command;
     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"
    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 case "$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     ;;
   114 esac
   115 
   116 exit "$RC"