[isabelle-dev] Document generation / Tags
makarius at sketis.net
Thu Sep 6 12:09:52 CEST 2012
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
>> 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.
More information about the isabelle-dev