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
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.
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
again
* Completely remove the document_output directory
* Execute again "isabelle build -c -o document=false". Now it will
work again.
It seems that some tool in the build chain could be more aggressive in
cleaning up stuff.
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
