Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
2 tasks done
keram opened this issue Jun 13, 2024 · 0 comments
Open
2 tasks done

Comments

@keram
Copy link
Contributor

keram commented Jun 13, 2024

  • I have read CONTRIBUTING.md.
  • 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant