REPL Start/Reload doesn't load current file

[ghost]

This happened after I updated to VSCode (current version 1.10.2), extension version 0.6.1
The :l command isn't sent to the console until after I exit Idris.

[zjhmale]

Hi @bascott, I can't reproduce your issue, I also work with VSCode 1.10.2 but I can kindly load the current file with this command, can you give a more detailed description of your issue, IIRC, you use Windows right? Probably it is OS sensitive issue?

[zjhmale]

BTW, what do you mean by until after I exit Idris? Thanks in advance 😄

[ghost]

@zjhmale Yes, I'm on Windows 10. Basically, when I use the command to start the REPL, it starts up in the command line, and then nothing happens. Then I type in :q in the REPL and get an error message:

The term ":l" is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name, or if a path was included, verify that the path is correct and try again.

At line:1 char:1
+ :l <path-to-current-file>
+ ~~
    + CategoryInfo          : ObjectNotFound: (:l:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException`

So my assumption was that the Extension opens up Idris on the command line then sends the load command (:l) to the REPL using the path to the current file, but the load command doesn't get sent unless I quit the REPL using :q.

[zjhmale]

Hi @bascott, it seems things go differently between OSX and Windows and I still can not wrap up the issue around my head unless I can see a screenshot or I can try this on a windows 10 machine by myself. The start repl code is here, can you kindly add a windows sensitive patch to that function? Cause I have no windows machine by my hand right now 😅 Thanks in advance!

[zjhmale]

@be5invis Will you also get the same issue here?

[ghost]

@zjhmale I've noticed that they changed the default terminal in Windows for VSCode 1.9.1 from cmd.exe to PowerShell. When I switched back to cmd.exe, it's working fine, so it seems to be a bug on the VSCode side when using the PowerShell terminal.

Edit: I've opened an issue on the VSCode side microsoft/vscode#23809

[zjhmale]

@bascott Thanks!