[isabelle] using makeindex in document preparation


I would like to use the glossaries LaTeX package through document

It needs

  pdflatex doc.tex
  makeindex -s doc.ist -o doc.gls doc.glo
  pdflatex doc.tex

to create the glossary in the document. isabelle latex in theory is capable
of running makeindex but it is not clear how the proper parameters can be

In lib/Tools/latex there is

function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }

but FILEBASE is only

FILEBASE="$(basename "$FILE" .tex)"

An idea is to write a Makefile into output/document with the above command
sequence. Is there any better?

Isabelle2014's LaTeX does not have the glossaries package but I copied it
from my own installation with the dependencies.


- Gergely

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.