ce75a23 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check for file extension in :e

Now, when Idris is invoked without a module file extension, :e will add it. Fixes #526.

commitce75a23933a258bffdd74c8c53fdb7875811ebe3 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 18 Oct 2013, 11:40 (13 years ago) parenta271f5d

1 file changed+4−1

compare with master

unifiedsplit

src/Idris/REPL.hs+4−1

src/Idris/REPL.hs+4−1

@@ -280,7 +280,7 @@ edit f orig

280280 let line = case errLine i of

281281 Just l -> " +" ++ show l ++ " "

282282 Nothing -> " "

283− let cmd = editor ++ line ++ f

283+ let cmd = editor ++ line ++ fixName f

284284 runIO $ system cmd

285285 clearErr

286286 putIState $ orig { idris_options = idris_options i

@@ -292,6 +292,9 @@ edit f orig

292292 where getEditor env | Just ed <- lookup "EDITOR" env = ed

293293 | Just ed <- lookup "VISUAL" env = ed

294294 | otherwise = "vi"

295+ fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file

296+ | otherwise = addExtension file "idr"

297+

295298

296299

297300proofs :: IState -> Idris ()