lib/Tools/latex
author wenzelm
Thu Jul 26 14:24:27 2012 +0200 (2012-07-26)
changeset 48515 3e17f343deb5
parent 40893 7d88ebdce380
child 52746 eec610972763
permissions -rwxr-xr-x
allow spaces in file names;
     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: dvi (default), dvi.gz, ps, ps.gz,"
    17   echo "                 pdf, bbl, idx, sty, syms"
    18   echo
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    20   echo "  producing the specified output format."
    21   echo
    22   exit 1
    23 }
    24 
    25 function fail()
    26 {
    27   echo "$1" >&2
    28   exit 2
    29 }
    30 
    31 
    32 ## process command line
    33 
    34 # options
    35 
    36 OUTFORMAT=dvi
    37 
    38 while getopts "o:" OPT
    39 do
    40   case "$OPT" in
    41     o)
    42       OUTFORMAT="$OPTARG"
    43       ;;
    44     \?)
    45       usage
    46       ;;
    47   esac
    48 done
    49 
    50 shift $(($OPTIND - 1))
    51 
    52 
    53 # args
    54 
    55 FILE="root.tex"
    56 [ "$#" -ge 1 ] && { FILE="$1"; shift; }
    57 
    58 [ "$#" -ne 0 ] && usage
    59 
    60 
    61 ## main
    62 
    63 # root file
    64 
    65 DIR="$(dirname "$FILE")"
    66 FILEBASE="$(basename "$FILE" .tex)"
    67 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
    68 
    69 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
    70 
    71 
    72 # operations
    73 
    74 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    75 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    76 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    77 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    78 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    79 function copy_styles ()
    80 {
    81   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
    82   do
    83     TARGET="$DIR"/$(basename "$STYLEFILE")
    84     perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
    85   done
    86 }
    87 
    88 function extract_syms ()
    89 {
    90   perl -n \
    91     -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    92     "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
    93   perl -n \
    94     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    95     "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
    96 }
    97 
    98 case "$OUTFORMAT" in
    99   dvi)
   100     check_root && \
   101     run_latex
   102     RC="$?"
   103     ;;
   104   dvi.gz)
   105     check_root && \
   106     run_latex && \
   107     gzip -f "$FILEBASE.dvi"
   108     RC="$?"
   109     ;;
   110   ps)
   111     check_root && \
   112     run_latex && \
   113     run_dvips
   114     RC="$?"
   115     ;;
   116   ps.gz)
   117     check_root && \
   118     run_latex && \
   119     run_dvips && \
   120     gzip -f "$FILEBASE.ps"
   121     RC="$?"
   122     ;;
   123   pdf)
   124     check_root && \
   125     run_pdflatex
   126     RC="$?"
   127     ;;
   128   bbl)
   129     check_root && \
   130     run_bibtex
   131     RC="$?"
   132     ;;
   133   idx)
   134     check_root && \
   135     run_makeindex
   136     RC="$?"
   137     ;;
   138   sty)
   139     copy_styles
   140     RC="$?"
   141     ;;
   142   syms)
   143     extract_syms
   144     RC="$?"
   145     ;;
   146   *)
   147     fail "Bad output format '$OUTFORMAT'"
   148     ;;
   149 esac
   150 
   151 exit "$RC"