.config/nvim/ftplugin/agda.vim

@@ -2,34 +2,23 @@
 " https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim
 " (Link is dead so use wayback machine)
 
-" To add more
-" https://www.compart.com/en/unicode/
-
 " 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
 imap <buffer> \_0 ₀
@@ -161,7 +150,26 @@ imap <buffer> \Chi Χ
 imap <buffer> \Psi Ψ
 imap <buffer> \Omega Ω
 
-" default cornelis mapping
+" autoload
+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>r :CornelisRefine<CR>
 nnoremap <buffer> <leader>d :CornelisMakeCase<CR>

.config/nvim/plugin/cornelis.vim

@@ -1,17 +0,0 @@
-" 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>"

nix/overlays/cornelis.nix

@@ -2,9 +2,4 @@
 let
   sources = import ../../npins;
 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

nix/overlays/iosevka/default.nix

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

npins/sources.json

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