search

derekelkins / agda-vim

Agda interaction in vim
BSD 2-Clause "Simplified" License
130 stars 47 forks source link

Extend the utf-8 file #31

Open nkaretnikov opened 6 years ago

nkaretnikov commented 6 years ago

I've come across this list of symbols: http://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html Would be nice to have them available.

I started searching for them because I needed the blackboard P. But this list lacks it, too.

Also, I think it would be nice to rewrite the file a bit, so it could be used for taking math notes. Similar to: https://github.com/dpiponi/math-vim/blob/master/math.vim The reason I want to use agda-vim's file is that I don't want to learn yet another set of mnemonics.

Right now, I can just :source the file, but there's no way of turning it off (besides exiting Vim).

How do you fill about these two things? If it continues bothering me, I might submit a patch.

derekelkins commented 6 years ago

I'm fine with accepting a pull request to add more entries to the agda-utf8.vim file. Adding the ability to toggle the whether the mappings are in force seems unnecessary and being used for math notes is out of scope of this. You should be able to quickly make a vim macro or even just a regex search and replace to produce an array that you can paste into Dan Piponi's file from the agda-utf8.vim file.