Add abbreviations

[WPettersson]

This allows vim to replace \pi with Π and similar. Firstly, to allow abbreviations with \, we need to add \ to iskeyword, so I modified the syntax file to only append to iskeyword rather than resetting it. Then in ftplugin/lean.vim we actually add \ to iskeyword, and create the abbreviations. I think I caught the useful ones, happy to add more if needed though.

[fmoralesc]

Great! Shouldn't the whole iskeyword definition move to ftplugin/lean.vim, though?

[WPettersson]

I'll be honest, I don't know exactly why the iskeyword definition even existed, so I didn't feel comfortable moving it. If the changes to iskeyword in syntax/lean.vim are required to have syntax highlighting working properly, then I think it should stay there. If it is not necessary for syntax highlighting, then I think it could be removed completely.

[fmoralesc]

Even if they are necessary for highlighting to work properly, it won't hurt to move them around: if I remember correctly, the ftplugin file will be loaded before the syntax file is loaded (actually, they are different files mostly for organization: technically, you could just define syntax elements in the ftplugin, for example). I'm guessing whoever created the syntax file didn't care to create an ftplugin file because it would have been just two lines.

I think the same thing applies to the expandtab setting in the syntax file.

[WPettersson]

You're right, the definition of iskeyword definitely can be moved around at will. Should I then move iskeyword and expandtab to ftplugin.vim?

[fmoralesc]

I think that would be cleaner overall.

[fmoralesc]

Two other things:

1. I think you need to add <buffer> to the abbreviations, so they don't bleed into other filetypes (currently they are defined globally). So, like this:

inoabbrev <buffer> \to →

2. Maybe add an abbreviation for λ? (lean uses fun).

[WPettersson]

I've added to the abbreviations, and an abbreviation for λ in the abbreviations commit, and I've also moved settings into ftplugin/lean.vim

[Julian]

I know folks don't really use this generally (though I just got this + coc.nvim working fairly easily for at least a basic setup) -- on the off chance someone does... this PR looks interesting though maybe these days copying the translations.json from the vscode repo leads to a bit more functionality and sharing.

I see the emacs code doesn't do that (maybe it should too?) -- gonna give that a shot here though should be straightforward to load the inoreabbrevs from there?

EDIT while I still remember: I ditched that idea given that there are some more abbreviations in the modern translations.json that won't work without modifying iskeyword, which is a bit of a sledgehammer, so instead I just plugged them into snippets via ultisnips/coc-snippets. So far so good there. LASTEDIT: I put what I did here: https://github.com/Julian/lean-unicode.vim

[adelejackson]

LASTEDIT: I put what I did here: https://github.com/Julian/lean-unicode.vim

Thanks for this! I found it very helpful.

[Julian]

Glad to hear. It does work quite well. I'm in the midst myself of moving to using native neovim LSP, during which I'll likely make a new version which uses vim-vsnip, which you might also be interested in (not sure when I'll get to it, I'm doing a bunch of things at once, but it'll hit my dotfiles at some point soon if you're interested).