How to accept unicode input without moving cursor?

[buggymcbugfix]

Say I wanted to write ⟨⟨ as an identifier.

Typing \ < \ < results in ⟨\<, so what I do is enter the following sequence of characters:

\ < [SPC] [BKSPC] \ <

Is there some key to accept the current input which would allow me not to have to space and backspace?

[buggymcbugfix]

PS: I tried esc but that doesn't do anything.

[buggymcbugfix]

PS': in the specific case of entering two consecutive non-Ascii characters, like above, it seems that I shouldn't even need to escape out of the special input mode, since \ always terminates it. (?)

[banacorn]

I see! I'll make it easier to terminate the input method!

[buggymcbugfix]

Hey, I think at some point you mentioned that it may be possible to factor out the input method part of this package? I think this would be really useful for use in other contexts. Currently it only works in files with .agda extension. Is this something that's already possible and if not, how doable is this? I would love to help but I'm by no means a JS whizz.

[banacorn]

The picture I had in mind is to make this input method an extension ("Provider") of the Autocomplete+ package. All we have to do is create a new package that work together with its Provider API. However the UI will be a lot different from what we have in agda-mode (in case you are expecting anything).

[buggymcbugfix]

I don't really mind the UX of Autocomplete+. Is it possible to use the backslash with Autocomplete+ though? I tried making snippets that start with backslash and they don't seem to complete.

[banacorn]

I'll see if I have time to try this out this weekend!

[buggymcbugfix]

Let me know if you need any input/help. We would like to use this with granule.

[banacorn]

cool!!

[banacorn]

You can now also exit the input method by pressing RETURN and ESC.