lib/Tools/latex
changeset 52746 eec610972763
parent 48515 3e17f343deb5
child 67264 449a989f42cd
     1.1 --- a/lib/Tools/latex	Sat Jul 27 22:16:04 2013 +0200
     1.2 +++ b/lib/Tools/latex	Sat Jul 27 22:20:25 2013 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4    echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 -  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     1.8 -  echo "                 pdf, bbl, idx, sty, syms"
     1.9 +  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty, syms"
    1.10    echo
    1.11    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    1.12    echo "  producing the specified output format."
    1.13 @@ -33,7 +32,7 @@
    1.14  
    1.15  # options
    1.16  
    1.17 -OUTFORMAT=dvi
    1.18 +OUTFORMAT=pdf
    1.19  
    1.20  while getopts "o:" OPT
    1.21  do
    1.22 @@ -75,7 +74,6 @@
    1.23  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    1.24  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    1.25  function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    1.26 -function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    1.27  function copy_styles ()
    1.28  {
    1.29    for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
    1.30 @@ -96,35 +94,16 @@
    1.31  }
    1.32  
    1.33  case "$OUTFORMAT" in
    1.34 +  pdf)
    1.35 +    check_root && \
    1.36 +    run_pdflatex
    1.37 +    RC="$?"
    1.38 +    ;;
    1.39    dvi)
    1.40      check_root && \
    1.41      run_latex
    1.42      RC="$?"
    1.43      ;;
    1.44 -  dvi.gz)
    1.45 -    check_root && \
    1.46 -    run_latex && \
    1.47 -    gzip -f "$FILEBASE.dvi"
    1.48 -    RC="$?"
    1.49 -    ;;
    1.50 -  ps)
    1.51 -    check_root && \
    1.52 -    run_latex && \
    1.53 -    run_dvips
    1.54 -    RC="$?"
    1.55 -    ;;
    1.56 -  ps.gz)
    1.57 -    check_root && \
    1.58 -    run_latex && \
    1.59 -    run_dvips && \
    1.60 -    gzip -f "$FILEBASE.ps"
    1.61 -    RC="$?"
    1.62 -    ;;
    1.63 -  pdf)
    1.64 -    check_root && \
    1.65 -    run_pdflatex
    1.66 -    RC="$?"
    1.67 -    ;;
    1.68    bbl)
    1.69      check_root && \
    1.70      run_bibtex