'dirty' error message ([idris/idris])

[michelrandahl]

when getting a type error, my error message in vim looks like this:

|| datastore.idr:62:48-49: [idris/idris]
|| When checking right hand side of Main.case block in case block in parsePrefix at datastore.idr:57:8 at datastore.idr:60:14 with expected type [idris/idris]
||         Maybe (Char, String) [idris/idris]
|| When checking argument a to constructor Builtins.MkPair: [idris/idris]
||         Type mismatch between [idris/idris]
||                 (A, B) (Type of (a, b)) [idris/idris]
||         and [idris/idris]
||                 Char (Expected type) [idris/idris]
|| datastore.idr:108:1-8:When checking left hand side of display: [idris/idris]
|| When checking an application of Main.display: [idris/idris]
||         Type mismatch between [idris/idris]
||                 (A, B) (Type of (a, b)) [idris/idris]
||         and [idris/idris]
||                 Char (Expected type) [idris/idris]

Is it possible to get those error messages without having [idris/idris] written all over the place? (is it perhaps my vim setup that's causing all this noise in the output?)

[yacinehmito]

What is displayed if you reload the file in the REPL instead of using Vim? Does it appear aswell?

[michelrandahl]

reloading in the repl is the same output, just without the [idris/idris] stuff

[michelrandahl]

I am using GNOME Terminal and Vim-bootstrap http://vim-bootstrap.com/ if that has anything to say

[yacinehmito]

I can't tell you why it does this. However, I think it might be related to syntastic. idris is the name of the language but also the name of the checker, which would explain an [idris/idris] at the end of every line.

Try disabling some syntastic options in your .vimrc to see if one is responsible.