[isabelle-dev] document_output vs. old document_dump/document_dump_mode

[Makarius]

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