d745c2e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

d745c2eEdwin Brady12 years ago

idris.cabal+3

compare with master

unifiedsplit

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

455 test/interactive006/input

456 test/interactive006/*.idr

457 test/interactive006/expected

458+ test/interactive007/run

459+ test/interactive007/input

460+ test/interactive007/expected

458

461

459 test/io001/run

462 test/io001/run

460 test/io001/*.idr

463 test/io001/*.idr

src/Idris/Error.hs−1

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

5import Prelude hiding (catch)

6import Idris.AbsSyntax

7import Idris.Delaborate

8−import Idris.Output

10import Idris.Core.Evaluate (ctxtAlist)

9import Idris.Core.Evaluate (ctxtAlist)

11import Idris.Core.TT

10import Idris.Core.TT

src/Idris/Parser.hs+8−9

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

220-}

221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

222syntaxDecl syn = do s <- syntaxRule syn

223− i <- get

223+ i <- get

224 put (i `addSyntax` s)

225 fc <- getFC

226− return (PSyntax fc s)

226+ return (PSyntax fc s)

227

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

229addSyntax :: IState -> Syntax -> IState

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

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

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

1204loadModule f

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

1205+ = idrisCatch (loadModule' f)

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

1207 ist <- getIState

1208 iWarn (getErrSpan e) $ pprintErr ist e

1209 return Nothing)

1210

1211{- | Load idris module -}

1212−loadModule' :: FilePath -> Idris String

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

1213loadModule' f

1214 = do i <- getIState

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

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

1217 ids <- allImportDirs

1218 fp <- findImport ids ibcsd file

1219 if file `elem` imported i

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

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

1221+ return Nothing

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

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

1222 case fp of

1223 case fp of

1223 IDR fn -> loadSource False fn Nothing

1224 IDR fn -> loadSource False fn Nothing

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

1228 case src of

1229 case src of

1229 IDR sfn -> loadSource False sfn Nothing

1230 IDR sfn -> loadSource False sfn Nothing

1230 LIDR sfn -> loadSource True sfn Nothing)

1231 LIDR sfn -> loadSource True sfn Nothing)

1231− let (dir, fh) = splitFileName file

1232+ return $ Just file

1232− return (dropExtension fh)

1233−

1234

1233

1235{- | Load idris code from file -}

1234{- | Load idris code from file -}

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

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

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

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

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

1270 ids <- allImportDirs

1269 ids <- allImportDirs

1271 ibcsd <- valIBCSubDir i

1270 ibcsd <- valIBCSubDir i

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

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

1273 do fp <- findImport ids ibcsd f

1272 do fp <- findImport ids ibcsd f

1274 case fp of

1273 case fp of

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

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

src/Idris/REPL.hs+2−1

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

629 Success (Right Reload) ->

630 do putIState $ orig { idris_options = idris_options i

631 , idris_colourTheme = idris_colourTheme i

632+ , imported = imported i

632 }

633 }

633 clearErr

634 clearErr

634 mods <- loadInputs inputs Nothing

635 mods <- loadInputs inputs Nothing

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

1181

1182

1182process fn (Apropos pkgs a) =

1183process fn (Apropos pkgs a) =

1183 do orig <- getIState

1184 do orig <- getIState

1184− when (not (null pkgs)) $

1185+ when (not (null pkgs)) $

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

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

1186 mapM_ loadPkgIndex pkgs

1187 mapM_ loadPkgIndex pkgs

1187 ist <- getIState

1188 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