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

[Gerwin Klein]

On 29/08/2012, at 10:21 PM, Makarius <makarius at sketis.net> wrote:

> 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'll have a look at document/build, it sounds like it provides everything I need.


> (I've never seen this situation in the conversions of old scripts in the past couple of weeks.)

By their nature you wouldn't find these in Isabelle or AFP. For me at least, they are usually bigger LaTeX setups that include a smaller Isabelle-generated part. If something is checked into the Isabelle repository or submitted to AFP, the relationship is the other way around and it is usually fairly natural to have isabelle as the dominant part.

Gerwin