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

[Tobias Nipkow]

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
epstopdf:

lapbroy100:Doc nipkow$ isabelle logo -o isabelle.pdf xxx
isabelle.pdf
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.

Tobias

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