39c07a7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proper REPL module reloading

Fixes #1587

commit39c07a7913b36f7cf4c0fcd5b0ea9da5c06cdd2c authorDmitry Bushev <bushevdv@gmail.com> dateThu 15 Jan 2015, 01:16 (12 years ago) parent2fd3ebc

7 files changed+20−11

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Error.hs−1 src/Idris/Parser.hs+8−9 src/Idris/REPL.hs+2−1 test/interactive007/expected+1 test/interactive007/input+4 test/interactive007/run+2

idris.cabal+3

@@ -455,6 +455,9 @@ Extra-source-files:

455455 test/interactive006/input

456456 test/interactive006/*.idr

457457 test/interactive006/expected

458+ test/interactive007/run

459+ test/interactive007/input

460+ test/interactive007/expected

458461

459462 test/io001/run

460463 test/io001/*.idr

src/Idris/Error.hs−1

@@ -5,7 +5,6 @@ module Idris.Error where

55import Prelude hiding (catch)

66import Idris.AbsSyntax

77import Idris.Delaborate

8−import Idris.Output

109import Idris.Core.Evaluate (ctxtAlist)

1110import Idris.Core.TT

src/Idris/Parser.hs+8−9

@@ -221,10 +221,10 @@ decl' syn = fixity

221221-}

222222syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

223223syntaxDecl syn = do s <- syntaxRule syn

224− i <- get

224+ i <- get

225225 put (i `addSyntax` s)

226226 fc <- getFC

227− return (PSyntax fc s)

227+ return (PSyntax fc s)

228228

229229-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.

230230addSyntax :: IState -> Syntax -> IState

@@ -1203,14 +1203,14 @@ parseProg syn fname input mrk

12031203{- | Load idris module and show error if something wrong happens -}

12041204loadModule :: FilePath -> Idris (Maybe String)

12051205loadModule f

1206− = idrisCatch (fmap Just (loadModule' f))

1206+ = idrisCatch (loadModule' f)

12071207 (\e -> do setErrSpan (getErrSpan e)

12081208 ist <- getIState

12091209 iWarn (getErrSpan e) $ pprintErr ist e

12101210 return Nothing)

12111211

12121212{- | Load idris module -}

1213−loadModule' :: FilePath -> Idris String

1213+loadModule' :: FilePath -> Idris (Maybe String)

12141214loadModule' f

12151215 = do i <- getIState

12161216 let file = takeWhile (/= ' ') f

@@ -1218,7 +1218,8 @@ loadModule' f

12181218 ids <- allImportDirs

12191219 fp <- findImport ids ibcsd file

12201220 if file `elem` imported i

1221− then iLOG $ "Already read " ++ file

1221+ then do iLOG $ "Already read " ++ file

1222+ return Nothing

12221223 else do putIState (i { imported = file : imported i })

12231224 case fp of

12241225 IDR fn -> loadSource False fn Nothing

@@ -1229,9 +1230,7 @@ loadModule' f

12291230 case src of

12301231 IDR sfn -> loadSource False sfn Nothing

12311232 LIDR sfn -> loadSource True sfn Nothing)

1232− let (dir, fh) = splitFileName file

1233− return (dropExtension fh)

1234−

1233+ return $ Just file

12351234

12361235{- | Load idris code from file -}

12371236loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

@@ -1270,7 +1269,7 @@ loadSource lidr f toline

12701269 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in

12711270 ids <- allImportDirs

12721271 ibcsd <- valIBCSubDir i

1273− mapM_ (\(re, f) ->

1272+ mapM_ (\(re, f) ->

12741273 do fp <- findImport ids ibcsd f

12751274 case fp of

12761275 LIDR fn -> ifail $ "No ibc for " ++ f

src/Idris/REPL.hs+2−1

@@ -623,6 +623,7 @@ processInput cmd orig inputs efile

623623 Success (Right Reload) ->

624624 do putIState $ orig { idris_options = idris_options i

625625 , idris_colourTheme = idris_colourTheme i

626+ , imported = imported i

626627 }

627628 clearErr

628629 mods <- loadInputs inputs Nothing

@@ -1175,7 +1176,7 @@ process fn (SetConsoleWidth w) = setWidth w

11751176

11761177process fn (Apropos pkgs a) =

11771178 do orig <- getIState

1178− when (not (null pkgs)) $

1179+ when (not (null pkgs)) $

11791180 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

11801181 mapM_ loadPkgIndex pkgs

11811182 ist <- getIState

test/interactive007/expectednew file+1

@@ -0,0 +1 @@

1+Idris> *Data/ZZ> *Data/ZZ> *Data/ZZ> *Data/ZZ> Bye bye

test/interactive007/inputnew file+4

@@ -0,0 +1,4 @@

1+:module Data.ZZ

2+:module Data.ZZ

3+:r

4+:module Data.ZZ

test/interactive007/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris --nobanner --nocolor < input