lib/Tools/latex
changeset 7865 d9be8bc5624e
parent 7857 a49a3978fe3a
child 8564 37a1e855390a
equal deleted inserted replaced
7864:5cd5a27f5c93 7865:d9be8bc5624e
    12   echo
    12   echo
    13   echo "Usage: $PRG [OPTIONS] [FILE]"
    13   echo "Usage: $PRG [OPTIONS] [FILE]"
    14   echo
    14   echo
    15   echo "  Options are:"
    15   echo "  Options are:"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    17   echo "                 pdf, or bbl"
    17   echo "                 pdf, bbl, png"
    18   echo
    18   echo
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    20   echo "  producing the specified output format."
    20   echo "  producing the specified output format."
    21   echo
    21   echo
    22   exit 1
    22   exit 1
    76 
    76 
    77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
       
    81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    81 
    82 
    82 
    83 
    83 # process file
    84 # process file
    84 
    85 
    85 case "$OUTFORMAT" in
    86 case "$OUTFORMAT" in
   109     ;;
   110     ;;
   110   bbl)
   111   bbl)
   111     run_bibtex
   112     run_bibtex
   112     RC=$?
   113     RC=$?
   113     ;;
   114     ;;
       
   115   png)
       
   116     run_thumbpdf
       
   117     RC=$?
       
   118     ;;
   114   *)
   119   *)
   115     fail "Bad output format '$OUTFORMAT'"
   120     fail "Bad output format '$OUTFORMAT'"
   116     ;;
   121     ;;
   117 esac
   122 esac
   118 
   123