idris-lang/Idris-dev — pull request #921 by david-christiansen (2014-02-22 08:58:14+00:00)
Title: Parser warnings; especially for invalid doc comments

This patch adds:

* A facility for non-fatal parser warnings
* A convenient way to add specific warnings for invalid documentation
comments
* Warnings for module doc comments (which are not currently supported)

This doesn't totally take care of #912, because I still need to insert more warning locations, but it's a good start. In particular, it gives a nice error message for @walkie's issue.