mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 05:01:34 +03:00
Recover the original way of sending file contexts to idemode clients
This commit is contained in:
parent
f0af11ac7e
commit
9512683e96
@ -1,7 +1,8 @@
|
|||||||
module Idris.REPL.Common
|
module Idris.REPL.Common
|
||||||
|
|
||||||
import Core.Env
|
|
||||||
import Core.Context.Log
|
import Core.Context.Log
|
||||||
|
import Core.Directory
|
||||||
|
import Core.Env
|
||||||
import Core.InitPrimitives
|
import Core.InitPrimitives
|
||||||
import Core.Metadata
|
import Core.Metadata
|
||||||
import Core.Primitives
|
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
|
-- TODO: Display a better message when the error doesn't contain a location
|
||||||
case map toNonEmptyFC (getFC a) of
|
case map toNonEmptyFC (getFC a) of
|
||||||
Nothing => iputStrLn msg
|
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",
|
send f (SExpList [SymbolAtom "warning",
|
||||||
SExpList [toSExp (show file),
|
SExpList [toSExp {a = String} fname,
|
||||||
toSExp (addOne startPos),
|
toSExp (addOne startPos),
|
||||||
toSExp (addOne endPos),
|
toSExp (addOne endPos),
|
||||||
toSExp !(renderWithoutColor msg),
|
toSExp !(renderWithoutColor msg),
|
||||||
|
Loading…
Reference in New Issue
Block a user