idris-hackers/idris-mode — pull request #131 by david-christiansen (2014-05-02 18:50:01+00:00)
Title: Display "can't find import" errors in warnings buffer instead of REPL

Fixes #48 once idris-lang/idris-dev#1180 gets merged.