Merge pull request #1531 from Russoul/fc-name-at

Reconcile FC and IDE mode

src/Core/Directory.idr

@@ -106,8 +106,8 @@ nsToPath loc ns
             | Nothing => pure (Left (ModuleNotFound loc ns))
          pure (Right f)
 
--- Given a namespace, return the full path to the source module (if it
--- exists in the working directory)
+-- Given a namespace, return the path to the source module relative
+-- to the working directory, if the module exists.
 export
 nsToSource : {auto c : Ref Ctxt Defs} ->
              FC -> ModuleIdent -> Core String

src/Idris/IDEMode/REPL.idr

@@ -8,6 +8,7 @@ import Compiler.Common
 import Core.AutoSearch
 import Core.CompileExpr
 import Core.Context
+import Core.Directory
 import Core.InitPrimitives
 import Core.Metadata
 import Core.Normalise
@@ -43,6 +44,7 @@ import TTImp.TTImp
 import TTImp.ProcessDecls
 
 import Libraries.Utils.Hex
+import Libraries.Utils.Path
 
 import Data.List
 import System
@@ -397,18 +399,34 @@ displayIDEResult outf i (REPL $ ConsoleWidthSet mn)
 displayIDEResult outf i (NameLocList dat)
   = printIDEResult outf i $ SExpList !(traverse (constructSExp . map toNonEmptyFC) dat)
   where
-    -- Can't recover the full path to the file, because
-    -- the name may come from an out-of-project location whereas we only store
-    -- module identifiers (source location is lost).
-    sexpOriginDesc : OriginDesc -> String
-    sexpOriginDesc (PhysicalIdrSrc mod) = show mod
-    sexpOriginDesc (PhysicalPkgSrc fname) = fname
-    sexpOriginDesc (Virtual Interactive) = "(Interactive)"
+    -- In order to recover the full path to the module referenced by FC,
+    -- which stores a module identifier as opposed to a full path,
+    -- we need to check the project's source folder and all the library directories
+    -- for the relevant source file.
+    -- (!) Always returns the *absolute* path.
+    sexpOriginDesc : OriginDesc -> Core String
+    sexpOriginDesc (PhysicalIdrSrc modIdent) = do
+      defs <- get Ctxt
+      let wdir = defs.options.dirs.working_dir
+      let pkg_dirs = filter (/= ".") defs.options.dirs.extra_dirs
+      let exts = map show listOfExtensions
+      Just fname <- catch
+          (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first
+          -- if not found, try looking for the file amongst the loaded packages.
+          (const $ firstAvailable $ do
+            pkg_dir <- pkg_dirs
+            let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir
+            ext <- exts
+            pure (pkg_dir_abs </> ModuleIdent.toPath modIdent <.> ext))
+        | _ => pure "(File-Not-Found)"
+      pure fname
+    sexpOriginDesc (PhysicalPkgSrc fname) = pure fname
+    sexpOriginDesc (Virtual Interactive) = pure "(Interactive)"
 
     constructSExp : (Name, NonEmptyFC) -> Core SExp
     constructSExp (name, origin, (startLine, startCol), (endLine, endCol)) = pure $
         SExpList [ StringAtom !(render $ pretty name)
-                 , StringAtom (sexpOriginDesc origin)
+                 , StringAtom !(sexpOriginDesc origin)
                  , IntegerAtom $ cast $ startLine
                  , IntegerAtom $ cast $ startCol
                  , IntegerAtom $ cast $ endLine

src/Idris/REPL/Common.idr

@@ -1,7 +1,8 @@
 module Idris.REPL.Common
 
-import Core.Env
 import Core.Context.Log
+import Core.Directory
+import Core.Env
 import Core.InitPrimitives
 import Core.Metadata
 import Core.Primitives
@@ -80,9 +81,19 @@ emitProblem a replDocCreator idemodeDocCreator getFC
                      -- TODO: Display a better message when the error doesn't contain a location
                      case map toNonEmptyFC (getFC a) of
                           Nothing => iputStrLn msg
-                          Just (file, startPos, endPos) =>
+                          Just (origin, startPos, endPos) => do
+                            fname <- case origin of
+                              PhysicalIdrSrc ident => do
+                                -- recover the file name relative to the working directory.
+                                -- (This is what idris2-mode expects)
+                                let fc = MkFC (PhysicalIdrSrc ident) startPos endPos
+                                catch (nsToSource fc ident) (const $ pure "(File-Not-Found)")
+                              PhysicalPkgSrc fname =>
+                                pure fname
+                              Virtual Interactive =>
+                                pure "(Interactive)"
                             send f (SExpList [SymbolAtom "warning",
-                                   SExpList [toSExp (show file),
+                                   SExpList [toSExp {a = String} fname,
                                             toSExp (addOne startPos),
                                               toSExp (addOne endPos),
                                               toSExp !(renderWithoutColor msg),