Compare commits

...

5 commits

5 changed files with 64 additions and 49 deletions

View file

@ -2,23 +2,34 @@
" https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim " https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim
" (Link is dead so use wayback machine) " (Link is dead so use wayback machine)
" To add more
" https://www.compart.com/en/unicode/
" Superscripts " Superscripts
imap <buffer> ^0 imap <buffer> \^0
imap <buffer> ^1 ¹ imap <buffer> \^1 ¹
imap <buffer> ^2 ² imap <buffer> \^2 ²
imap <buffer> ^3 ³ imap <buffer> \^3 ³
imap <buffer> ^4 imap <buffer> \^4
imap <buffer> ^5 imap <buffer> \^5
imap <buffer> ^6 imap <buffer> \^6
imap <buffer> ^7 imap <buffer> \^7
imap <buffer> ^8 imap <buffer> \^8
imap <buffer> ^9 imap <buffer> \^9
imap <buffer> ^+ imap <buffer> \^+
imap <buffer> ^- imap <buffer> \^-
imap <buffer> ^= imap <buffer> \^=
imap <buffer> ^( imap <buffer> \^(
imap <buffer> ^) imap <buffer> \^)
imap <buffer> ^n imap <buffer> \^n
imap <buffer> \^l ˡ
imap <buffer> \^r ʳ
imap <buffer> \'
imap <buffer> \''
imap <buffer> \''' ‴
imap <buffer> \''''
" Subscripts " Subscripts
imap <buffer> \_0 imap <buffer> \_0
@ -150,26 +161,7 @@ imap <buffer> \Chi Χ
imap <buffer> \Psi Ψ imap <buffer> \Psi Ψ
imap <buffer> \Omega Ω imap <buffer> \Omega Ω
" autoload " default cornelis mapping
function! CornelisLoadWrapper()
if exists(":CornelisLoad") ==# 2
CornelisLoad
endif
endfunction
au BufReadPre *.agda call CornelisLoadWrapper()
au BufReadPre *.lagda* call CornelisLoadWrapper()
au BufRead,BufNewFile *.agda call AgdaFiletype()
au BufRead,BufNewFile *.lagda* call AgdaFiletype()
au QuitPre *.agda :CornelisCloseInfoWindows
au QuitPre *.lagda* :CornelisCloseInfoWindows
" autoreload at file write
au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"
au BufWritePost *.lagda* execute "normal! :CornelisLoad\<CR>"
" default cornelis config
nnoremap <buffer> <leader>l :CornelisLoad<CR> nnoremap <buffer> <leader>l :CornelisLoad<CR>
nnoremap <buffer> <leader>r :CornelisRefine<CR> nnoremap <buffer> <leader>r :CornelisRefine<CR>
nnoremap <buffer> <leader>d :CornelisMakeCase<CR> nnoremap <buffer> <leader>d :CornelisMakeCase<CR>

View file

@ -0,0 +1,17 @@
" agda related autocommands
function! CornelisLoadWrapper()
if exists(":CornelisLoad") ==# 2
CornelisLoad
endif
endfunction
au BufReadPre *.agda call CornelisLoadWrapper()
au BufReadPre *.lagda* call CornelisLoadWrapper()
au QuitPre *.agda :CornelisCloseInfoWindows
au QuitPre *.lagda* :CornelisCloseInfoWindows
" autoreload at file write
au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"
au BufWritePost *.lagda* execute "normal! :CornelisLoad\<CR>"

View file

@ -2,4 +2,9 @@
let let
sources = import ../../npins; sources = import ../../npins;
in in
# If this is updated, we break split on case support for PLFA.
# PLFA uses 2.7.0
# https://github.com/agda/cornelis/issues/169
assert sources.cornelis.version == "v2.7.1";
sources.cornelis.asFlake.overlays.cornelis sources.cornelis.asFlake.overlays.cornelis

View file

@ -29,18 +29,18 @@ let
identityOverlay = _: _: { }; identityOverlay = _: _: { };
overlays = overlays =
lib.crossLists let
( # Useless complexity just for the fun
spacingCfg: variantCfg: n-airyToList = acc: x: {
lib.composeManyExtensions [ value = acc ++ [ x ];
spacingCfg __functor = self: n-airyToList self.value;
variantCfg };
] combinations = lib.crossLists (n-airyToList [ ]) [
)
[
(import ./spacings.nix) (import ./spacings.nix)
([ identityOverlay ] ++ import ./variants.nix) ([ identityOverlay ] ++ import ./variants.nix)
]; ];
in
map ({ value, ... }: lib.composeManyExtensions value) combinations;
iosevkas = lib.genAttrs' overlays ( iosevkas = lib.genAttrs' overlays (
overlay: overlay:

View file

@ -27,10 +27,11 @@
"version_upper_bound": null, "version_upper_bound": null,
"release_prefix": null, "release_prefix": null,
"submodules": false, "submodules": false,
"version": "v2.8.0", "version": "v2.7.1",
"revision": "67137c76fe0d4a8bb899eea46afaa370993d3556", "revision": "40298eed11eb877526b3ab3f648d8a7bff9e2f50",
"url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.8.0", "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.7.1",
"hash": "sha256-dGS6De3EtTirgEMDMSjA+iBNc670W7pG4eA02Nq7Azo=" "hash": "sha256-h18AeggnOSSjy0RLJIkWsSID1BJTarOV9F1APKusIrE=",
"frozen": true
}, },
"disko": { "disko": {
"type": "GitRelease", "type": "GitRelease",