ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 22:47:12 +03:00
Code Issues Projects Releases Wiki Activity

Canonicalize paths in internalapp

Browse Source 
Otherwise, equal pathnames would not show up as equal, leading to
problems in interactive editing if Idris's notion of a relative path
didn't agree with the user's notion. For example, loading a file as
"Foo/Bar.idr" would break interactive editing, because Idris would
remember the name as "./Foo/Bar.idr".
This commit is contained in:
David Raymond Christiansen 2015-06-08 16:56:58 +02:00
parent d03295d652
commit 34f516d570
1 changed files with 18 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/Idris/AbsSyntax.hs
View File

@ -16,6 +16,7 @@ import Util.DynamicLinker
import System.Console.Haskeline
import System.IO
import System.Directory (canonicalizePath, doesFileExist)
import Control.Applicative
import Control.Monad (liftM3)
@ -516,14 +517,26 @@ getName = do i <- getIState;
addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
addInternalApp fp l t
= do i <- getIState
putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
-- We canonicalise the path to make "./Test/Module.idr" equal
-- to "Test/Module.idr"
exists <- runIO $ doesFileExist fp
when exists $
do fp' <- runIO $ canonicalizePath fp
putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })
getInternalApp :: FilePath -> Int -> Idris PTerm
getInternalApp fp l = do i <- getIState
case lookup (fp, l) (idris_lineapps i) of
Just n' -> return n'
Nothing -> return Placeholder
-- TODO: What if it's not there?
-- We canonicalise the path to make
-- "./Test/Module.idr" equal to
-- "Test/Module.idr"
exists <- runIO $ doesFileExist fp
if exists
then do fp' <- runIO $ canonicalizePath fp
case lookup (fp', l) (idris_lineapps i) of
Just n' -> return n'
Nothing -> return Placeholder
-- TODO: What if it's not there?
else return Placeholder
-- Pattern definitions are only used for coverage checking, so erase them
-- when we're done