Documentation Coverage Warning Flag

[jfdm]

Idris is documentation aware, this an annoyingly beneficial feature. Using this functionality, it would be beneficial when developing libraries to have a documentation coverage warning flag of the form:

$ idris --warndoc <level> ...

where <level> is one of:

Level	Description
none	No documentation is required. The default setting.
public	All public and abstract elements must be documented`
all	All objects must be documented.

This flag would be used to ensure that the library has been documented to one of the aforementioned levels. While this is naturally beneficial to library developers, it can also be beneficial for the oft-discussed Idris package manager. Packages can be uploaded if --warndoc public produces no warnings.

Of course the final form is open to debate.

This should be flagged as feature request and patches welcome.

[david-christiansen]

Great idea!