Adding a clause for an operator does not work

[justjoheinz]

Given

infixl 5 :|:
(:|:) : Nat -> Nat

and trying to add a clause with the cursor inside the brackets results in

Idris Error: does not understand

[justjoheinz]

@david-christiansen Could you help me here please? If I just send :|: to idris I get the Idris Error: does not understand reply, but when I send (:|:) idris replies with ((:|:)) k = ?op_rhs

In emacs everything works as expected, but I can't imagine that the emacs mode strips unrequired parantheses from the response.

[justjoheinz]

@david-christiansen I tried my outlined approach with this PR and it seems to work, but I really would like to have other developers opinion on this. It feels weird.
@archaeron , please feel free to have a look as well.

[david-christiansen]

I wonder why this isn't working... the Emacs mode doesn't do it this way.

Here's a bit of a log from an add-clause command in the Emacs mode:

module whatever

data Foo = MkFoo Integer

infixr 8 ++++

(++++) : Nat -> Nat -> Nat

I then issue add-clause with the cursor on the operator, and Emacs sends this:

((:add-clause 7 "++++") 18)

Idris replies with this:

(:return (:ok "(++++) k j = ?op_rhs") 18)

Your example works fine too:

09:17:31 -> ((:add-clause 12 ":|:")
 23)
09:17:31 <- (:return
 (:ok "(:|:) k = ?op_rhs")
 23)

So I'm not sure why it would need that. Can you post a log of the message being sent?

[justjoheinz]

Your ++++ example works without my PR.
the :|: example works like this:

000018((:add-clause 4 :|:) 6)
(:return (:error "did not understand") 6)

So from what I gather the difference is that emacs quotes the ":|:" (which seems correct) and atom doesn't. So my fix is futile, and it would be sufficient to quote the word.
Thank you very much!

[david-christiansen]

Yes, names should always be passed as strings.

…

On Fri, Sep 7, 2018, 09:58 Markus Klink ***@***.***> wrote: Your ++++ example works without my PR. the :|: example works like this: 000018((:add-clause 4 :|:) 6) (:return (:error "did not understand") 6) So from what I gather the difference is that emacs quotes the ":|:" (which seems correct) and atom doesn't. So my fix is futile, and it would be sufficient to quote the word. Thank you very much! — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#185 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAHCggvj6bIo35SBYIUe36d3l9ZhL5NXks5uYqWugaJpZM4O8T-o> .