[isabelle] using makeindex in document preparation



Hi,

I would like to use the glossaries LaTeX package through document
preparation.

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
passed.

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.

Cheers

- Gergely



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