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

Tobias Nipkow nipkow at in.tum.de
Thu Aug 30 16:16:24 CEST 2012

Am 29/08/2012 14:21, schrieb 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.

I just tried to by looking into the System manual, but that was the wrong place.
Where should I look?

BTW, the latest version of the logo tool triggers a bug in older versions of

lapbroy100:Doc nipkow$ isabelle logo -o isabelle.pdf xxx
epstopdf ($Id: epstopdf.pl 15843 2009-10-19 23:14:41Z karl $) 2.11
!!! Error: Cannot open standard input

Will have to figure out how to upgrade my latex installation.


>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list