Closed Kazark closed 4 years ago
Good thought. I am not sure if the comint repl does not support :browse because of the compiler or for some other reason. I will do some investigating and see if we can allow it.
The Idris IDE protocol doesn't expose :browse over the REPL because it has a dedicated command for it. In Emacs, you can get this by right-clicking an identifier in the namespace you want to browse or by using M-x idris-browse-namespace. The Emacs interface is better than the REPL one: it has little expansion buttons next to each sub-namespace, for instance.
I think the right thing to do is probably to make the REPL command :browse display the same result as the built-in protocol command.
IOW I think this is more of a discoverability issue than anything.
Fixed with PR https://github.com/idris-lang/Idris-dev/pull/4873
@conjunctive thank you!
On Windows, with 0.300.0@25.3.1 (spacemacs)--and also on my Linux box, with an older version of Spacemacs--I get this result from
:browse
:So for the longest time, I have been starting a secondary Idris process through my terminal when I've needed to browse a namespace! In the process of coming to request the addition off
:browse
, I found by searching this repository that I can doSPC SPC idris-browse-namespace
, and I'm quite happy with the results. However, perhaps if the:browse
is not to be supported in the REPL as actually producing the results, it could at least be intercepted with a message telling n00bs like me aboutidris-browse-namespace
. (I hope I am right in ascertaining that this is not an issue with Spacemacs having an older version of this plug-in: based on searching this repo, it did not seem like it was supported through the REPL.)