On Thu, 6 Sep 2012, Lars Noschinski wrote:
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.
With document=false it should not fail here. I think you have
document=pdf hardwired in ROOT, which takes precedence. Such persistent
document options are exactly what you do for private paper/slides
sessions, but not for public ones (Isabelle repository or AFP).
* 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.
It is the intended behaviour of document_output. The idea is to model the
old-fashioned situation where you lump together a lot of tex sources and
run some of the tex tools on it (latex, bibtex etc.), until you are
satisfied with the result.
This means intermediate states need to be preserved, even if they might
contain junk. In that case you do "rm -rf output" manually.
I've come across the description of the "aggressive" option -c of isabelle
document recently here
http://isabelle.in.tum.de/repos/isabelle/rev/342ca8f3197b#l4.272 and was
unsure about the delicate distinction in the behaviour. It will probably
become more clear when document preparation is done interactively, and
related reforms for it emerging.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
