[isabelle-dev] NEWS: session 'document_files'

Makarius makarius at sketis.net
Fri Apr 11 13:30:11 CEST 2014

* 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 ".")

The default for the "in" notation above is still "document", in accordance 
to what we have in Isabelle + AFP, and "isabelle mkroot".


More information about the isabelle-dev mailing list