atom-language-idris icon indicating copy to clipboard operation
atom-language-idris copied to clipboard

Published 20 hours ago • verified publisher icon idris-hackers

changeDirectory() doesn't work with Idris 2

Open memoryallocator opened this issue 3 years ago • 2 comments

The idris2's :cd command requires a quoted string, but the changeDirectory() function does not surround the dir variable with quotes. As a result of this, there are the errors:

Expected string begin.

(Interactive):1:5--1:6
 1 | :cd /home/demo/Documents/Idris2

More than that, if the directory path contains a quote (for example, /"tmp), the plugin hangs at Idris: opening REPL ....

memoryallocator avatar Mar 25 '22 13:03 memoryallocator

The corresponding change in emacs idris-mode: https://github.com/idris-hackers/idris-mode/commit/762eda0a047f25ac76854f86ad3a1c7910b96c95#diff-57c9b17a4d33ee59f640d96a562f576b22d600b5adb02038a989e8eb1d2e76c5R89

jmanuel1 avatar Feb 19 '24 05:02 jmanuel1

I think the compiler is restarted every time any of the compilerOptions change, including the source directory, which makes the invocation of :cd redundant. And currently, I can't reproduce this bug, even though I've hit it before. In fact, I can't tell if that code path is even executed.

jmanuel1 avatar Feb 21 '24 06:02 jmanuel1