[isabelle-dev] NEWS: session 'document_files'

Makarius makarius at sketis.net
Fri Apr 11 23:52:00 CEST 2014


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.


 	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.tar.gz
Type: application/octet-stream
Size: 373 bytes
Desc: 
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140411/40c73f4c/attachment-0002.obj>


More information about the isabelle-dev mailing list