101f5f9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2355 from david-christiansen/interactive-fix

101f5f9David Christiansen11 years ago

src/Idris/AbsSyntax.hs+18−5

compare with master

unifiedsplit

@@ -16,6 +16,7 @@ import Util.DynamicLinker

17import System.Console.Haskeline

18import System.IO

19+import System.Directory (canonicalizePath, doesFileExist)

20import Control.Applicative

21import Control.Applicative

21import Control.Monad (liftM3)

22import Control.Monad (liftM3)

@@ -516,14 +517,26 @@ getName = do i <- getIState;

516addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

517addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

517addInternalApp fp l t

518addInternalApp fp l t

518 = do i <- getIState

519 = do i <- getIState

520+ -- We canonicalise the path to make "./Test/Module.idr" equal

521+ -- to "Test/Module.idr"

522+ exists <- runIO $ doesFileExist fp

523+ when exists $

524+ do fp' <- runIO $ canonicalizePath fp

519− putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })

525+ putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })

520

526

521getInternalApp :: FilePath -> Int -> Idris PTerm

527getInternalApp :: FilePath -> Int -> Idris PTerm

522getInternalApp fp l = do i <- getIState

528getInternalApp fp l = do i <- getIState

529+ -- We canonicalise the path to make

530+ -- "./Test/Module.idr" equal to

531+ -- "Test/Module.idr"

532+ exists <- runIO $ doesFileExist fp

533+ if exists

534+ then do fp' <- runIO $ canonicalizePath fp

523− case lookup (fp, l) (idris_lineapps i) of

535+ case lookup (fp', l) (idris_lineapps i) of

524− Just n' -> return n'

536+ Just n' -> return n'

525− Nothing -> return Placeholder

537+ Nothing -> return Placeholder

526− -- TODO: What if it's not there?

538+ -- TODO: What if it's not there?

539+ else return Placeholder

527

540

528-- Pattern definitions are only used for coverage checking, so erase them

541-- Pattern definitions are only used for coverage checking, so erase them

529-- when we're done

542-- when we're done

src/Idris/REPL.hs+4−2

@@ -573,8 +573,10 @@ splitName s = case reverse $ splitOn "." s of

573idemodeProcess :: FilePath -> Command -> Idris ()

574idemodeProcess fn Warranty = process fn Warranty

575idemodeProcess fn Help = process fn Help

576−idemodeProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

576+idemodeProcess fn (ChangeDirectory f) =

577+ do process fn (ChangeDirectory f)

578+ dir <- runIO $ getCurrentDirectory

577− iPrintResult "changed directory to"

579+ iPrintResult $ "changed directory to " ++ dir

578idemodeProcess fn (ModImport f) = process fn (ModImport f)

580idemodeProcess fn (ModImport f) = process fn (ModImport f)

579idemodeProcess fn (Eval t) = process fn (Eval t)

581idemodeProcess fn (Eval t) = process fn (Eval t)

580idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)

582idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)