Known issues of the --mkdoc command

[gallais]

In case people want to have a look, the bulk of the command is implemented
in Idris.Doc.String (for the :doc command that the --mkdoc command reuses)
and Idris.Doc.HTML.

Copy/pasted from the original PR (#903):

• types are not shown where they should be
  (although most of the time, the type is in the first line of the documentation)
  [NDLA: Not sure what this means?]
• "documentation" is currently just a <pre> tag with the output equivalent to :doc in the REPL
• namespace members are sorted alphabetically, this may not be the best choice
  [NDLA e.g. we could use file position instead to have a more scope-friendly presentation.
  This would also allow us to include things like headers in between sections]
• --clean does not remove the generated docs
• code needs some cleanup (and probably moved into a separate file, as it pollutes
  Package.idr with lots of HTML output-specific code, which will get worse as more
  features are implemented)

Additional issues:

• Each doc file corresponds to a physical file and only contains the definitions in that
  exact namespace. We should either fully embrace the namespace-based approach and have
  one file per namespace or make sure the doc file also contains the definitions introduced
  in a nested namespace

[gallais]

#2411 addresses

1. alphabetical order of definitions (now changed to FC's startPos order)
2. content of namespace rather than source file

[Matthew-Mosior]

#3353 addresses --clean does not remove the generated docs.