idris-hackers/idris-mode — pull request #74 by trillioneyes (2014-01-31 02:20:23+00:00)
Title: Prevented extra indentation after a `module` declaration.

This should fix #72.

I found the nature of the fix alarming, so an explanation: in `haskell-mode`, a module-declaration-parser must handle not only things such as `module Hands where` but also `module Hands (feet, Eyes(..)) where`. In this setting, a check to make sure that the end of the module declaration (the symbol `end-tokens` in the code) had been reached. As far as I'm aware, Idris module declarations can't be decorated in any way, so the indentation should return to top-level mode unconditionally after reading the module name, and we can just remove the check.