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

[Gerwin Klein]

On 28/08/2012, at 8:06 PM, Makarius wrote:

> Are there remaining uses (or users) of the old document_dump / document_dump_mode options?  This corresponds to former options -D and -C of isabelle usedir.
> 
> The meaning of these features has become quite difficult to define, so it looks like they are better discontinued.
> 
> If there are remaining cases of difficult IsaMakefile/usedir configurations that still use them, they can be discussed here to see if anything is still missing in the new build tool to replace them.

I use -D/document_dump extensively for producing papers. The Isabelle Latex output pretty much always requires post processing for anything that has higher type setting requirements. My standard setup these days is not to use root.tex for papers, but only to generate .tex from .thy, then post-process, then include manually in a master .tex file. 

It looks like document_dump with default "all" for document_dump_mode produces what I need, though (even "tex" would be sufficient).

Tobias and I had a setup where we also needed isabelle.sty, but we could subsume that with document_output. 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.

Cheers,
Gerwin