[isabelle-dev] NEWS: session 'document_files'

[Tobias Nipkow]

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? Something like "document=tex" as an alternative to
"document=pdf" comes to mind.

Thanks
Tobias

On 11/04/2014 13:30, Makarius wrote:
> * Session ROOT specifications support explicit 'document_files' for
> robust dependencies on LaTeX sources.  Only these explicitly given
> files are copied to the document output directory, before document
> processing is started.
> 
> 
> This refers to Isabelle/cd8b6d849b6a.  That changeset also contains some
> documentation in the "system" manual. Some examples are in 3ff16a7f0b2e for the
> src/Doc directory, with its traditional complication of matters -- and it got
> again a bit simpler.  As expected, there were a few mistakes in the informal
> specification of dependencies on 'files', which was a left-over from the bad old
> times of "make".
> 
> I am putting the 'document_files' reform here on the table for inspection and
> discussion.  If no further aspects are arising that require change of syntax or
> semantics of the mechanism, I will update all Isabelle + AFP session ROOT files
> eventually, lets say 2 weeks from now.
> 
> 
> Occasionally some users have asked about evading the canonical "document"
> directory for the source template.  This can be now done like this
> 
>   document_files (in ".")
>     "root.tex"
> 
> The default for the "in" notation above is still "document", in accordance to
> what we have in Isabelle + AFP, and "isabelle mkroot".
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev