8e550c1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Trim trailing whitespace in parseCmd

When auto-completing a filename to :load from the REPL, the trailing space added by the auto-completion will be ignored for actually loading the file, but a subsequent invocation of :edit will use the path including the space, leading to the creation of a new file "<module>.idr .idr". This problem is easily fixed by trimming not just leading, but also trailing whitespace in parseCmd.

commit8e550c1959d223f24a28cc22d71b0d05d1d189c5 authorJohannes Griebler <johannes.griebler@gmail.com> dateFri 19 Jun 2015, 14:58 (11 years ago) parent5457da9

1 file changed+6−1

compare with master

unifiedsplit

src/Idris/REPLParser.hs+6−1

src/Idris/REPLParser.hs+6−1

@@ -25,7 +25,12 @@ import Data.Char(isSpace, toLower)

2525import qualified Data.ByteString.UTF8 as UTF8

2626

2727parseCmd :: IState -> String -> String -> Result (Either String Command)

28−parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace

28+parseCmd i inputname = P.runparser pCmd i inputname . trim

29+ where trim = fst . foldr f ("", True) . dropWhile isSpace

30+ where f e (xs, False) = (e : xs, False)

31+ f e (xs, True)

32+ | isSpace e = (xs, True)

33+ | otherwise = (e : xs, False)

2934

3035type CommandTable = [ ( [String], CmdArg, String

3136 , String -> P.IdrisParser (Either String Command) ) ]