[isabelle-dev] Document generation / Tags

[Makarius]

On Thu, 6 Sep 2012, Lars Noschinski wrote:

> On 06.09.2012 10:20, Florian Haftmann wrote:
>>> I see "isabelle document" has a simple option to switch on/off various
>>> things in the generated document (for example, proofs). Is there a way
>>> to supply these directly from the ROOT file? Would be useful for these
>>> one-off use cases (e.g. I want a view on my theory omitting all the
>>> proofs).
>> 
>> what about option document_variants?
>
> document_variants seems to be about the file name of the generated document.

The variants have names and tags to modify certain ranges of the text.
See option -V in old usedir in the system manual.

The manual is basically already updated for the new build system, but some 
of its parts are still disconnected.  In particular some overview of how 
the new options environment affects the build process is missing, which 
would have been document_variants here.


 	Makarius