Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Make output of ide-mode `:interpret` consistent to always return consistent datatype (String)

Open keram opened this issue 8 months ago • 0 comments

  • [X] I have read CONTRIBUTING.md.
  • [X] I have checked that there is no existing PR/issue about my proposal.

Summary

Making the signature of output of ((:interpret String) Int) to be in form of (:return (:ok String) Int) or (:return (:error String) Int)

Motivation

The interpret command is used to pass input from user in emacs idris-repl and output is printed back to user Currently the :interpret command returns either a string

-> ((:interpret ":cwd") 71)
 <- (:return (:ok "Current working directory is \"/x/sources/Idris2/src\"") 71)

displayed in repl to user as

λΠ> :cwd
Current working directory is "/X/sources/Idris2/src"

or data structure

-> ((:interpret ":version") 72)
<- (:return (:ok ((0 7 0)   ("055568be2"))) 72)

which leads to an error in editor: error in process filter: Wrong type argument: char-or-string-p, ((0 7 0) ("055568be2")) because the function processing output from Idris expects string.

The proposal

Make signature of the :interpret X consistent as mentioned above (:return (:ok|error String) Int) and return data structre as` result of invokign specific command directly. Good example of this is getting a version of Idris2

Input: (:version 1) -> Expected output: (:return (:ok ((0 7 0) ("055568be2"))) 1) 🆗

Input ((:interpret ":version") 1) -> Expected output: (:return (:ok "0.7.0-055568be2") 1), Currently: (:return (:ok ((0 7 0) ("055568be2"))) 1) 🚫

Examples

From the list of commands :? I'm aware so far that version and opts returns the data structures leading to error in processing

Technical implementation

Alternatives considered

Update the processing function in idris-mode to keep state of what output from Idris2 is related to and try to format in presentable format to user. This would add extra complexity to the idris-mode, harder asyn processing and possible inconsistencies in user experience between different editors using the ide-mode.

Alternatives considered

Making the signature consistent will make easier to build and maintain editor plugins together with better user experience

keram avatar Jun 13 '24 23:06 keram