run makeindex if necessary

--- a/etc/settings	Wed Jan 07 07:52:12 2004 +0100
+++ b/etc/settings	Thu Jan 08 04:32:52 2004 +0100
@@ -85,6 +85,9 @@
 # bibtex command for isatool latex/document
 ISABELLE_BIBTEX="bibtex"
 
+# makeindex command for isatool latex/document
+ISABELLE_MAKEINDEX="makeindex"
+
 # dvips command for isatool latex/document
 ISABELLE_DVIPS="dvips -D 600"
 

--- a/lib/Tools/document	Wed Jan 07 07:52:12 2004 +0100
+++ b/lib/Tools/document	Thu Jan 08 04:32:52 2004 +0100
@@ -83,11 +83,12 @@
 function pre_latex ()
 {
   local FMT="$1"
-  [ -n "$CLEAN" ] && rm -f *.aux *.out
+  [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind
   "$ISATOOL" latex -o sty && \
   "$ISATOOL" latex -o "$FMT" && \
   { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
-  "$ISATOOL" latex -o "$FMT"
+  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \  
+    "$ISATOOL" latex -o "$FMT"
 }
 
 (

--- a/lib/Tools/latex	Wed Jan 07 07:52:12 2004 +0100
+++ b/lib/Tools/latex	Thu Jan 08 04:32:52 2004 +0100
@@ -76,6 +76,7 @@
 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
+function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
@@ -115,6 +116,11 @@
     run_bibtex
     RC="$?"
     ;;
+  idx)
+    check_root && \
+    run_makeindex
+    RC="$?"
+    ;;
   png)
     check_root && \
     run_thumbpdf