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

git.iko.soy/Idris-dev

on master help sign in

Proper REPL module reloading

39c07a7Dmitry Bushev12 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

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

221-}

222syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

223syntaxDecl syn = do s <- syntaxRule syn

224− i <- get

224+ i <- get

225 put (i `addSyntax` s)

226 fc <- getFC

227− return (PSyntax fc s)

227+ return (PSyntax fc s)

228

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

230addSyntax :: IState -> Syntax -> IState

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

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

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

1205loadModule f

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

1206+ = idrisCatch (loadModule' f)

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

1208 ist <- getIState

1209 iWarn (getErrSpan e) $ pprintErr ist e

1210 return Nothing)

1211

1212{- | Load idris module -}

1213−loadModule' :: FilePath -> Idris String

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

1214loadModule' f

1215 = do i <- getIState

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

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

1218 ids <- allImportDirs

1219 fp <- findImport ids ibcsd file

1220 if file `elem` imported i

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

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

1222+ return Nothing

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

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

1223 case fp of

1224 case fp of

1224 IDR fn -> loadSource False fn Nothing

1225 IDR fn -> loadSource False fn Nothing

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

1229 case src of

1230 case src of

1230 IDR sfn -> loadSource False sfn Nothing

1231 IDR sfn -> loadSource False sfn Nothing

1231 LIDR sfn -> loadSource True sfn Nothing)

1232 LIDR sfn -> loadSource True sfn Nothing)

1232− let (dir, fh) = splitFileName file

1233+ return $ Just file

1233− return (dropExtension fh)

1234−

1235

1234

1236{- | Load idris code from file -}

1235{- | Load idris code from file -}

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

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

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

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

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

1271 ids <- allImportDirs

1270 ids <- allImportDirs

1272 ibcsd <- valIBCSubDir i

1271 ibcsd <- valIBCSubDir i

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

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

1274 do fp <- findImport ids ibcsd f

1273 do fp <- findImport ids ibcsd f

1275 case fp of

1274 case fp of

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

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

src/Idris/REPL.hs+2−1

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

623 Success (Right Reload) ->

624 do putIState $ orig { idris_options = idris_options i

625 , idris_colourTheme = idris_colourTheme i

626+ , imported = imported i

626 }

627 }

627 clearErr

628 clearErr

628 mods <- loadInputs inputs Nothing

629 mods <- loadInputs inputs Nothing

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

1175

1176

1176process fn (Apropos pkgs a) =

1177process fn (Apropos pkgs a) =

1177 do orig <- getIState

1178 do orig <- getIState

1178− when (not (null pkgs)) $

1179+ when (not (null pkgs)) $

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

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

1180 mapM_ loadPkgIndex pkgs

1181 mapM_ loadPkgIndex pkgs

1181 ist <- getIState

1182 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