[isabelle-dev] document_output vs. old document_dump/document_dump_mode
makarius at sketis.net
Wed Aug 29 14:12:49 CEST 2012
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.)
More information about the isabelle-dev