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

[Makarius]

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.


 	Makarius