lib/Tools/latex
changeset 14344 0f0a2148a099
parent 12846 0fce95478e19
child 14921 4ad751fa50c1
equal deleted inserted replaced
14343:6bc647f472b9 14344:0f0a2148a099
    74 # operations
    74 # operations
    75 
    75 
    76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
       
    79 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    79 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    80 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    80 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    81 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    82 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    82 
    83 
    83 case "$OUTFORMAT" in
    84 case "$OUTFORMAT" in
   113   bbl)
   114   bbl)
   114     check_root && \
   115     check_root && \
   115     run_bibtex
   116     run_bibtex
   116     RC="$?"
   117     RC="$?"
   117     ;;
   118     ;;
       
   119   idx)
       
   120     check_root && \
       
   121     run_makeindex
       
   122     RC="$?"
       
   123     ;;
   118   png)
   124   png)
   119     check_root && \
   125     check_root && \
   120     run_thumbpdf
   126     run_thumbpdf
   121     RC="$?"
   127     RC="$?"
   122     ;;
   128     ;;