d745c2e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1852 from 4e6/repl-module-reload

Proper REPL module reloading

commitd745c2e00ee4d7f58c2f439ce869a7b77aaed96b authorEdwin Brady <edwin.brady@gmail.com> dateSat 31 Jan 2015, 12:28 (12 years ago) parent9c80995 39c07a7

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

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

220220-}

221221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

222222syntaxDecl syn = do s <- syntaxRule syn

223− i <- get

223+ i <- get

224224 put (i `addSyntax` s)

225225 fc <- getFC

226− return (PSyntax fc s)

226+ return (PSyntax fc s)

227227

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

229229addSyntax :: IState -> Syntax -> IState

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

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

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

12041204loadModule f

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

1205+ = idrisCatch (loadModule' f)

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

12071207 ist <- getIState

12081208 iWarn (getErrSpan e) $ pprintErr ist e

12091209 return Nothing)

12101210

12111211{- | Load idris module -}

1212−loadModule' :: FilePath -> Idris String

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

12131213loadModule' f

12141214 = do i <- getIState

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

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

12171217 ids <- allImportDirs

12181218 fp <- findImport ids ibcsd file

12191219 if file `elem` imported i

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

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

1221+ return Nothing

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

12221223 case fp of

12231224 IDR fn -> loadSource False fn Nothing

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

12281229 case src of

12291230 IDR sfn -> loadSource False sfn Nothing

12301231 LIDR sfn -> loadSource True sfn Nothing)

1231− let (dir, fh) = splitFileName file

1232− return (dropExtension fh)

1233−

1232+ return $ Just file

12341233

12351234{- | Load idris code from file -}

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

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

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

12701269 ids <- allImportDirs

12711270 ibcsd <- valIBCSubDir i

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

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

12731272 do fp <- findImport ids ibcsd f

12741273 case fp of

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

src/Idris/REPL.hs+2−1

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

629629 Success (Right Reload) ->

630630 do putIState $ orig { idris_options = idris_options i

631631 , idris_colourTheme = idris_colourTheme i

632+ , imported = imported i

632633 }

633634 clearErr

634635 mods <- loadInputs inputs Nothing

@@ -1181,7 +1182,7 @@ process fn (SetConsoleWidth w) = setWidth w

11811182

11821183process fn (Apropos pkgs a) =

11831184 do orig <- getIState

1184− when (not (null pkgs)) $

1185+ when (not (null pkgs)) $

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

11861187 mapM_ loadPkgIndex pkgs

11871188 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