banacorn / language-agda

Agda language support for the Atom editor
https://atom.io/packages/language-agda
MIT License
13 stars 5 forks source link

Unicode input with two or more cursors #13

Closed jonaprieto closed 6 years ago

jonaprieto commented 6 years ago

I use to replace text using ctrl+D to select the same matches for example. But with the cursors that the atom puts, when I try to write some Unicode character, what I got is that only in the last line (last match) the Unicode appears. Why?

For example,

A
...
A

After selecting the As with two cursors (symbol |)

A|
...
A|

And if I try to type \_1 instead of

A₁
...
A₁

This is what I got

A₁
...
A_1
banacorn commented 6 years ago

Because it never came to me that that we can type unicode symbols simultaneously at different places XD

Did some quick survey, here's the problem:

const selectedRange = this.editor.getSelectedBufferRange();

Here's the solution!:

const selectedRange = this.editor.getSelectedBufferRanges();