[isabelle-dev] NEWS: session 'document_files'

[Makarius]

On Sun, 13 Apr 2014, Tobias Nipkow wrote:

> That works fine, thank you.
>
> Tobias
>
> On 11/04/2014 23:52, Makarius wrote:
>> On Fri, 11 Apr 2014, Tobias Nipkow wrote:
>>
>>> What I sometimes need is to have the latex files generated but not processed.
>>> Currently I achieve this with a dummy root.tex file that includes nothing. Is
>>> there a less dummy way?
>>
>> There is no need for root.tex and latex to produce a dummy root.pdf. This can be
>> done more directly via some document/build script that merely does "touch
>> root.pdf".  See the included example session.
>>
>> That is functionality from the summer 2012 reform, and I am rather glad that the
>> number of build options was successfully reduced, while it has become more general.
>>
>> If there is a strong need for it, one could add some option to the "isabelle
>> mkroot" tool to produce such a setup -- it presently uses only 2 letters of the
>> alphabet for options.

Just to conclude this side-thread, here is also the relavant snippet from 
the "system" manual in Isabelle/282f3b06fa86:

   In more complex situations, a separate @{verbatim build} script for
   the document sources may be given.  It is invoked with command-line
   arguments for the document format and the document variant name.
   The script needs to produce corresponding output files, e.g.\
   @{verbatim root.pdf} for target format @{verbatim pdf} (and default
   variants).  The main work can be again delegated to @{tool latex},
   but it is also possible to harvest generated {\LaTeX} sources and
   copy them elsewhere.

I've required several minutes to find it, even though I knew it was there, 
but we have too many manuals anyway.

Nonetheless, there is no particular plan of action right now.


 	Makarius