Re: [isabelle] using makeindex in document preparation



On Wed, 1 Jul 2015, Gergely Buday wrote:

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

Makefiles are a historical misunderstanding. It is better to forget that they ever existed.

The Isabelle document preparation allows to define a specific build function, just by putting a shell script (in fact any executable) of the right name in the right place.

See also the "system" manual:

  In more complex situations, a separate @{verbatim build} script for
  the document sources may be given.  It is invoked with command-line
  arguments for the document format and the document variant name.
  The script needs to produce corresponding output files, e.g.\
  @{verbatim root.pdf} for target format @{verbatim pdf} (and default
  variants).  The main work can be again delegated to @{tool latex},
  but it is also possible to harvest generated {\LaTeX} sources and
  copy them elsewhere.

You can take the document setup for this manual itself as an example: Isabelle2015/src/Doc/ROOT and Isabelle2015/src/Doc/System -- that is not the most simple version of such a "more complex situation", though.


	Makarius




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