run makeindex if necessary
authorkleing
Thu Jan 08 04:32:52 2004 +0100 (2004-01-08)
changeset 143440f0a2148a099
parent 14343 6bc647f472b9
child 14345 3023d90dc59e
run makeindex if necessary
etc/settings
lib/Tools/document
lib/Tools/latex
     1.1 --- a/etc/settings	Wed Jan 07 07:52:12 2004 +0100
     1.2 +++ b/etc/settings	Thu Jan 08 04:32:52 2004 +0100
     1.3 @@ -85,6 +85,9 @@
     1.4  # bibtex command for isatool latex/document
     1.5  ISABELLE_BIBTEX="bibtex"
     1.6  
     1.7 +# makeindex command for isatool latex/document
     1.8 +ISABELLE_MAKEINDEX="makeindex"
     1.9 +
    1.10  # dvips command for isatool latex/document
    1.11  ISABELLE_DVIPS="dvips -D 600"
    1.12  
     2.1 --- a/lib/Tools/document	Wed Jan 07 07:52:12 2004 +0100
     2.2 +++ b/lib/Tools/document	Thu Jan 08 04:32:52 2004 +0100
     2.3 @@ -83,11 +83,12 @@
     2.4  function pre_latex ()
     2.5  {
     2.6    local FMT="$1"
     2.7 -  [ -n "$CLEAN" ] && rm -f *.aux *.out
     2.8 +  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind
     2.9    "$ISATOOL" latex -o sty && \
    2.10    "$ISATOOL" latex -o "$FMT" && \
    2.11    { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
    2.12 -  "$ISATOOL" latex -o "$FMT"
    2.13 +  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \  
    2.14 +    "$ISATOOL" latex -o "$FMT"
    2.15  }
    2.16  
    2.17  (
     3.1 --- a/lib/Tools/latex	Wed Jan 07 07:52:12 2004 +0100
     3.2 +++ b/lib/Tools/latex	Thu Jan 08 04:32:52 2004 +0100
     3.3 @@ -76,6 +76,7 @@
     3.4  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     3.5  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     3.6  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
     3.7 +function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
     3.8  function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
     3.9  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    3.10  function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    3.11 @@ -115,6 +116,11 @@
    3.12      run_bibtex
    3.13      RC="$?"
    3.14      ;;
    3.15 +  idx)
    3.16 +    check_root && \
    3.17 +    run_makeindex
    3.18 +    RC="$?"
    3.19 +    ;;
    3.20    png)
    3.21      check_root && \
    3.22      run_thumbpdf