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.kl...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
