[isabelle-dev] document_output vs. old document_dump/document_dump_mode
makarius at sketis.net
Wed Aug 29 14:21:57 CEST 2012
On Wed, 29 Aug 2012, Gerwin Klein wrote:
> A small annoyance with document_output was that the output doesn't seem
> to get produced for document=false (i.e. seems to force a latex run) and
> that it insists on creating a "document" subdirectory in the target
> directory that I give it.
In fact it produces a sub-directory for each of the document_variants,
which is just "document" by default. The corresponding root.tex can be
optionally prefixed by that name, too. See afp/thys/Collections how it
is used there to produce unrelated documents.
You can also short-circuit things by using a dummy root.tex with something
like "touch roof.$FORMAT" in document/build, if you really need to run
latex outside of the session context. (I've never seen this situation in
the conversions of old scripts in the past couple of weeks.)
So it is worth taking a fresh look at document_output -- it achieves more
things with fewer options.
More information about the isabelle-dev