[isabelle-dev] Document generation / Tags

[Lars Noschinski]

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