[isabelle-dev] document_output vs. old document_dump/document_dump_mode
c-sterna at jaist.ac.jp
Wed Aug 29 09:00:01 CEST 2012
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
More information about the isabelle-dev