overlays/iosevka: useless refactor

.config/nvim/ftplugin/agda.vim

@@ -2,23 +2,34 @@
 " 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> ^1 ¹
-imap <buffer> ^2 ²
-imap <buffer> ^3 ³
-imap <buffer> ^4 ⁴
-imap <buffer> ^5 ⁵
-imap <buffer> ^6 ⁶
-imap <buffer> ^7 ⁷
-imap <buffer> ^8 ⁸
-imap <buffer> ^9 ⁹
-imap <buffer> ^+ ⁺
-imap <buffer> ^- ⁻
-imap <buffer> ^= ⁼
-imap <buffer> ^( ⁽
-imap <buffer> ^) ⁾
-imap <buffer> ^n ⁿ
+imap <buffer> \^0 ⁰
+imap <buffer> \^1 ¹
+imap <buffer> \^2 ²
+imap <buffer> \^3 ³
+imap <buffer> \^4 ⁴
+imap <buffer> \^5 ⁵
+imap <buffer> \^6 ⁶
+imap <buffer> \^7 ⁷
+imap <buffer> \^8 ⁸
+imap <buffer> \^9 ⁹
+imap <buffer> \^+ ⁺
+imap <buffer> \^- ⁻
+imap <buffer> \^= ⁼
+imap <buffer> \^( ⁽
+imap <buffer> \^) ⁾
+imap <buffer> \^n ⁿ
+
+imap <buffer> \^l ˡ
+imap <buffer> \^r ʳ
+
+imap <buffer> \' ′
+imap <buffer> \'' ″
+imap <buffer> \''' ‴
+imap <buffer> \'''' ⁗
 
 " Subscripts
 imap <buffer> \_0 ₀
@@ -150,26 +161,7 @@ imap <buffer> \Chi Χ
 imap <buffer> \Psi Ψ
 imap <buffer> \Omega Ω
 
-" 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
+" default cornelis mapping
 nnoremap <buffer> <leader>l :CornelisLoad<CR>
 nnoremap <buffer> <leader>r :CornelisRefine<CR>
 nnoremap <buffer> <leader>d :CornelisMakeCase<CR>

.config/nvim/plugin/cornelis.vim

@@ -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>"

nix/overlays/cornelis.nix

@@ -2,4 +2,9 @@
 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 =
-    lib.crossLists
-      (
-        spacingCfg: variantCfg:
-        lib.composeManyExtensions [
-          spacingCfg
-          variantCfg
-        ]
-      )
-      [
+    let
+      # Useless complexity just for the fun
+      n-airyToList = acc: x: {
+        value = acc ++ [ x ];
+        __functor = self: n-airyToList self.value;
+      };
+      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,10 +27,11 @@
       "version_upper_bound": null,
       "release_prefix": null,
       "submodules": false,
-      "version": "v2.8.0",
-      "revision": "67137c76fe0d4a8bb899eea46afaa370993d3556",
-      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.8.0",
-      "hash": "sha256-dGS6De3EtTirgEMDMSjA+iBNc670W7pG4eA02Nq7Azo="
+      "version": "v2.7.1",
+      "revision": "40298eed11eb877526b3ab3f648d8a7bff9e2f50",
+      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.7.1",
+      "hash": "sha256-h18AeggnOSSjy0RLJIkWsSID1BJTarOV9F1APKusIrE=",
+      "frozen": true
     },
     "disko": {
       "type": "GitRelease",