@mention autocompletion

[edemaine]

Requested in 6.851

[jbosboom]

Also requested from 6.892!

Some usernames don't correspond well to user (human) names, so ideally the autocomplete can search through both. That is, typing @jeffrey might suggest, along with any usernames starting/containing that string, also @jbosboom because it matches Jeffrey Bosboom. For each line in the autocomplete list, you can indicate what is being matched by bolding the matched substring; then lines can be sorted by how well-matched they are.

[edemaine]

Here's some documentation about how we can do this in CodeMirror:

https://stackoverflow.com/questions/13744176/codemirror-autocomplete-after-any-keyup

The tricky part seems to be deciding when to display the autocompletion hints. Presumably when you entered a key (including backspace) in a word starting with @. This seems to be Github's behavior (including completion by name, which stops when you hit space, so can only do one name).