idris-hackers/idris-mode — pull request #212 by david-christiansen (2014-07-16 08:31:20+00:00)
Title: Doc updates

* Added note about currently loaded region face
This is because it's a frequent complaint, but the feature is very nice if you load files partially.

* Add note about completion-ignored-extensions and .ibc files
This is based on a Twitter discussion with @jfdm and @dysinger