idris-vim icon indicating copy to clipboard operation
idris-vim copied to clipboard

Syntastic integration generates bogus command lines

Open cbiffle opened this issue 10 years ago • 0 comments

(idris-vim commit 45680a3c412f2cc8d40aff512e5e9ace44002922, Idris 0.9.19.)

The idris-vim Syntastic integration is generating command lines of the form

idris --client :l filename.idr

which causes Idris to bomb out with a usage message. (Unfortunately it returns 0 when it does so, so vim provides no indication that something's wrong.)

The command line needs to be of the form

idris --client ":l filename.idr"

because Idris appears to be processing individual argument strings as commands, not the entire set of arguments.

I've managed to fake this in the current version by abusing args and post_args to surround the command with quotes. This works only because Idris is tolerant of whitespace before and after filenames; it isn't clear how it would work with a filename e.g. containing whitespace.

cbiffle avatar Sep 06 '15 16:09 cbiffle