[isabelle-dev] Document generation / Tags
noschinl at in.tum.de
Thu Sep 6 14:24:39 CEST 2012
On 06.09.2012 12:09, Makarius wrote:
> 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
> The variants have names and tags to modify certain ranges of the text.
> See option -V in old usedir in the system manual.
Thanks; I've never really used document generation before, so I was not
aware of this.
Something else I discovered when I tried to use a build script:
* Add a script document/build producing an error
* Execute "isabelle build -c -o document=false" for your session. It
will obviously fail.
* Remove document/build
* Execute again "isabelle build -c -o document=false". It will fail
* Completely remove the document_output directory
* Execute again "isabelle build -c -o document=false". Now it will
It seems that some tool in the build chain could be more aggressive in
cleaning up stuff.
More information about the isabelle-dev