[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"
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
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
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 stringdisplayed in repl to user as
or data structure
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 Idris2Input:
(: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 thatversion
andopts
returns the data structures leading to error in processingTechnical 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