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

Fix ide mode repl not converting escaped characters (#665)

Browse Source
This commit is contained in:
Chetan Taralekar 2020-09-16 04:55:44 -05:00 committed by GitHub
parent ea0df039fe
commit 3c24bc5ed5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 11 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/IDEMode/Parser.idr
View File

@ -5,10 +5,12 @@ module Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Data.Maybe
import Data.List
import Data.Strings
import Parser.Lexer.Source
import Parser.Source
import Parser.Support
import Text.Lexer
import Text.Parser
import Utils.Either
@ -26,7 +28,7 @@ ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(stringLit, \x => StringLit (fromMaybe "" (escape (stripQuotes x)))),
(identAllowDashes, \x => Ident x),
(space, Comment)]

2
tests/Main.idr
View File

@ -146,7 +146,7 @@ nodeTests
ideModeTests : List String
ideModeTests
= [ "ideMode001", "ideMode002", "ideMode003" ]
= [ "ideMode001", "ideMode002", "ideMode003", "ideMode004" ]
preludeTests : List String
preludeTests

3
tests/ideMode/ideMode004/expected Normal file
View File

@ -0,0 +1,3 @@
000018(:protocol-version 2 0)
000021(:return (:ok "\"Test\"" ()) 32)
Alas the file is done, aborting

1
tests/ideMode/ideMode004/input Normal file
View File

@ -0,0 +1 @@
00001C((:interpret "\"Test\"") 32)

3
tests/ideMode/ideMode004/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --ide-mode < input
rm -rf build