idris-hackers/idris-mode — pull request #61 by trillioneyes (2014-01-25 09:58:04+00:00)
Title: Added indentation handling for the `record` keyword

Previously, in a situation such as the following:
```
record Hands : Type where|
```
pressing enter would cause idris-mode to complain of an `Illegal token: where`. It turned out that `idris-mode-indentation` was at least partially unaware of the `record` keyword. It should now handle this correctly.