[isabelle-dev] document_output vs. old document_dump/document_dump_mode

[Christian Sternagel]

On 08/29/2012 03:16 PM, Gerwin Klein wrote:
> On 28/08/2012, at 8:06 PM, Makarius wrote:
>
>> Are there remaining uses (or users) of the old document_dump / document_dump_mode options?  This corresponds to former options -D and -C of isabelle usedir.
>>
>> The meaning of these features has become quite difficult to define, so it looks like they are better discontinued.
>>
>> If there are remaining cases of difficult IsaMakefile/usedir configurations that still use them, they can be discussed here to see if anything is still missing in the new build tool to replace them.
>
> I use -D/document_dump extensively for producing papers.
Same here. I did however not come around yet to check how my 
"traditional" setup could be simulated (or better, improved) with the 
new build tool. - chris