agda-mode
agda-mode copied to clipboard
banacorn
Input Symbol only works from Cmd+Shift+P
I hope I am not missing something, but when I just type \, it does not realize I want to insert a symbol.
I need to open the palette to do so.
What do you mean by a palette? The panel that pops up after your loaded the file (ctrl-c ctrl-l) ?
The input method activates only when the file extension is .agda
Sorry I wasn't clear enough.
When I do Cmd + Shift + P, select Agda Mode: Input Symbol, and then type bn, it displays ℕ, but when I just type \bn, nothing happens (even after ^C ^L).
Edit: And the file extension is .agda so this is not the issue.
This is what the keybinding looks like on my editor, typing \ alone should be enough to invoke the input method.
Could you please share what your keybinding looks like?
As you can see, this is the same for me.
I am on Mac OS X Yosemite 10.10.4 (14E11f) using the last version of Atom and of your package.
Nope, it only does that with Cmd-Shift-P.
I have one warning related to your package, but I am not sure it had something to do with the bug at hand (which you don't have apparently?).
I've send a patch, please update to the latest version and see if the problem still persists
Thanks, but I am afraid nothing have changed (except that you have fixed all the warnings).
I just updated to the last version of your package, and it still doesn't work. Am I the only one having this problem?
Does other commands also have this problem, or is it just agda-mode:input-symbol ?
Is it possible that the keystroke got overridden by other packages, which also occupies \
No, I have tested them, and they seem to work just fine.
Apparently there is no keystroke on \ (but writing the \ itself of course), just one on cmd-\:
So okay, for me, the following work:
'atom-text-editor.agda':
'ctrl-:': 'agda-mode:input-symbol'
Apparently, \ isn't a valid keystroke (I tried to use it for newline, and it doesn't work either — and yes I wrote \\).
Even better:
'atom-text-editor.agda':
'alt-/': 'agda-mode:input-symbol'
This is the same combination as for \ and it actually works.
Thanks.
Thanks!
Does it has something to do with keyboard layouts? (localization, not physical layout) https://github.com/atom/atom-keymap/issues/35 https://github.com/atom/atom/issues/1625
\\ works fine for me and some of the others while alt-/ doesn't
But it's okay we will add both keystrokes to the keymap anyway!
I don't think so, but it is hard to tell.
Using the right alt doesn't change anything for me (it works with alt-/ and doesn't with \\).
It's been a while, and the codebase has changed a lot since then, is this still an issue?
Hi. It worked last time and it still does. I think it's because of the trick we mentioned earlier but it's not that bad is it?
It's true we could have closed the issue, I'll leave it to you.
Maybe I forgot something but I don't know how to remove the key binding alt-/ to test.
Oh, I added alt-/ on purpose dated back when you said it's the same combination as for \
Yes I do know that. I just don't know how to test if \ is now recognized on its own without this trick.
I just installed the newest atom-beta, language-agda and agda-mode and the problem persists. I have a Finnish keyboard layout, this might have something to do with the problem. When I Alt-press some keys, the key binding resolver gives me wrong keys for many non-letter keys and alt-shift-number combinations. The strange thing is, that when I press the key alone or shift-number alone, the correct character is printed, according to my keyboard layout. But for some reason the key binding resolver gets the wrong key from some other layout. As an example, I found out that Alt-' on my keyboard corresponds to Alt-/, so I can use that to enable agda character input mode, so I have a solution to the problem. However, this issue is not resolved since somehow the key binding resolver gets wrong keys. I have no idea where to start looking for the problem. I compiled from source and have the git repository cloned, so if anyone has any idea, I can give it a try.
Thank you for reporting this!
Do you have any other keyboard functional layouts, aside from the Finnish one?
I have a Taiwanese keyboard, with a visual layout labeled with exotic symbols:
There are 2 functional layouts I'm using: Taiwanese and US. I do everything with the US layout (including coding), and I switch to the Taiwanese layout only when I'm typing Chinese characters.
When I'm using the US layout, everything works fine. But I get weird symbols when I Alt- press every key with the Taiwanese layout.
Perhaps switching to the US functional layout would solve the problem, or we could also add another combination of keys that doesn't get in the way with the Finnish layout. :smile:
I only have the Finnish keyboard. I investigated some more, and it seems that with Alt-key, the 'key' is interpreted as if my keyboard had US layout. Without Alt, I get keys correctly as in Finnish layout. Very strange. I can work around the problem, but it would be nice to figure out why this happens.
Maybe it would be a good idea to install another functional layout (input method).
I get to switch my keyboard layout (input method) between the US and TW with a key combination (⌘ + space), which frees me from having to hold on to the alt key or something.
The plain old \ unicode sequences are working for me (us eng kbd), eg \bN types the nat N, etc
I'm closing this because I've rewritten the whole input system. Please reopen this issue if the problem still persists.