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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
