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