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

[Makarius]

On Wed, 29 Aug 2012, Lawrence Paulson wrote:

> This has always been my approach as well. Long ago I wrote a little 
> script for post-processing the latex files. Larry
>
> On 29 Aug 2012, at 07:16, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
>
>> 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.

When starting the thread I've put document_output in the subject, but 
forgot to say anything about it in the text.

>From what was reported so far, it all sounds like it could be done more 
directly with the new document_output option, together with some 
document/build script to do the pre/postprocessing.  Both are covered in 
the system manual already, and src/Doc provides some examples for 
intricate situations inherited from the past.

So document_output and document/build should be the real thing, not a 
simulation.  If it is not quite the real thing yet, I am open to 
suggestions, but preserving old behaviour and old habits is not worth it. 
(It is unclear what the old behaviour actually is, due to too many add-on 
options and sub-options.)


 	Makarius