idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 16:51:51 +03:00
Code Issues Projects Releases Wiki Activity

Do a tiny renaming

Browse Source
This commit is contained in:
russoul 2020-10-26 18:54:11 +03:00
parent 3cb30516e3
commit c8875c0f9d
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Idris/IDEMode/REPL.idr
View File

@ -142,7 +142,7 @@ data IDEResult
| NameList (List Name) | NameList (List Name)
| Term String -- should be a PTerm + metadata, or SExp. | Term String -- should be a PTerm + metadata, or SExp.
| TTTerm String -- should be a TT Term + metadata, or perhaps SExp | TTTerm String -- should be a TT Term + metadata, or perhaps SExp
| NamesInFiles (List (Name, FC)) | NameLocList (List (Name, FC))
replWrap : Core REPLResult -> Core IDEResult replWrap : Core REPLResult -> Core IDEResult
replWrap m = pure $ REPL !m replWrap m = pure $ REPL !m
@ -164,7 +164,7 @@ process (NameAt name Nothing)
= do defs <- get Ctxt = do defs <- get Ctxt
glob <- lookupCtxtName (UN name) (gamma defs) glob <- lookupCtxtName (UN name) (gamma defs)
let dat = map (\(name, _, gdef) => (name, gdef.location)) glob let dat = map (\(name, _, gdef) => (name, gdef.location)) glob
pure (NamesInFiles dat) pure (NameLocList dat)
process (NameAt n (Just _)) process (NameAt n (Just _))
= do todoCmd "name-at <name> <line> <column>" = do todoCmd "name-at <name> <line> <column>"
pure $ REPL $ Edited $ DisplayEdit emptyDoc pure $ REPL $ Edited $ DisplayEdit emptyDoc
@ -388,7 +388,7 @@ displayIDEResult outf i (REPL $ ConsoleWidthSet mn)
Just k => show k Just k => show k
Nothing => "auto" Nothing => "auto"
in printIDEResult outf i $ StringAtom $ "Set consolewidth to " ++ width in printIDEResult outf i $ StringAtom $ "Set consolewidth to " ++ width
displayIDEResult outf i (NamesInFiles dat) displayIDEResult outf i (NameLocList dat)
= printIDEResult outf i = printIDEResult outf i
$ SExpList !(traverse $ SExpList !(traverse
(\(name, fc) (\(name, fc)