Develop

README.md

@@ -10,6 +10,14 @@ this is non-trivial.
 
 1. Install [lua-utf8](https://github.com/starwing/luautf8) library on your system.
 
+for macOS, 
+
+```
+brew install lua@5.1 
+luarocks install  --lua-version 5.1  luautf8
+sudo rsync -av ~/.luarocks/lib/lua/5.1 /usr/local/lib/lua
+```
+
 2. Use a plugin manager such as [paq](https://github.com/savq/paq-nvim)
    and pass the name of this repository:
    ```lua

agda-input-x11.vim

@@ -0,0 +1,35 @@
+noremap! <buffer> <LocalLeader><S-~> 	∼
+noremap! <buffer> <LocalLeader><S-~>n 	≁
+noremap! <buffer> <LocalLeader><S-~>~ 	≈
+noremap! <buffer> <LocalLeader><S-~>~n 	≉
+noremap! <buffer> <LocalLeader><S-~> 	≋
+noremap! <buffer> <LocalLeader><S-~>- 	≃
+noremap! <buffer> <LocalLeader><S-~>-n 	≄
+noremap! <buffer> <LocalLeader><S-~>= 	≅
+noremap! <buffer> <LocalLeader><S-~>=n 	≇
+noremap! <buffer> <LocalLeader><S-~>~- 	≊
+noremap! <buffer> <LocalLeader><S-^>a       ᵃ
+noremap! <buffer> <LocalLeader><S-^>b       ᵇ
+noremap! <buffer> <LocalLeader><S-^>c       ᶜ
+noremap! <buffer> <LocalLeader><S-^>d       ᵈ
+noremap! <buffer> <LocalLeader><S-^>e       ᵉ
+noremap! <buffer> <LocalLeader><S-^>f       ᶠ
+noremap! <buffer> <LocalLeader><S-^>g       ᵍ
+noremap! <buffer> <LocalLeader><S-^>h       ʰ
+noremap! <buffer> <LocalLeader><S-^>i       ⁱ
+noremap! <buffer> <LocalLeader><S-^>j       ʲ
+noremap! <buffer> <LocalLeader><S-^>k       ᵏ
+noremap! <buffer> <LocalLeader><S-^>l       ˡ
+noremap! <buffer> <LocalLeader><S-^>m       ᵐ
+noremap! <buffer> <LocalLeader><S-^>n       ⁿ
+noremap! <buffer> <LocalLeader><S-^>o       ᵒ
+noremap! <buffer> <LocalLeader><S-^>p       ᵖ
+noremap! <buffer> <LocalLeader><S-^>r       ʳ
+noremap! <buffer> <LocalLeader><S-^>s       ˢ
+noremap! <buffer> <LocalLeader><S-^>t       ᵗ
+noremap! <buffer> <LocalLeader><S-^>u       ᵘ
+noremap! <buffer> <LocalLeader><S-^>v       ᵛ
+noremap! <buffer> <LocalLeader><S-^>w       ʷ
+noremap! <buffer> <LocalLeader><S-^>x       ˣ
+noremap! <buffer> <LocalLeader><S-^>y       ʸ
+noremap! <buffer> <LocalLeader><S-^>z       ᶻ

agda-input.vim

@@ -45,10 +45,12 @@ noremap! <buffer> <LocalLeader>ell  ℓ
 " https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html
 
 " Equality and similar symbols
+" somehow we cannot map ~ in neovim (why? )
 noremap! <buffer> <LocalLeader>=n 	≠
 noremap! <buffer> <LocalLeader>~ 	∼
 noremap! <buffer> <LocalLeader>~n 	≁
 noremap! <buffer> <LocalLeader>~~ 	≈
+noremap! <buffer> <LocalLeader>## 	≈
 noremap! <buffer> <LocalLeader>~~n 	≉
 noremap! <buffer> <LocalLeader>~ 	≋
 noremap! <buffer> <LocalLeader>:~ 	∻
@@ -254,6 +256,21 @@ noremap! <buffer> <LocalLeader>6 ₆
 noremap! <buffer> <LocalLeader>7 ₇
 noremap! <buffer> <LocalLeader>8 ₈
 noremap! <buffer> <LocalLeader>9 ₉
+noremap! <buffer> <LocalLeader>#- ⁻¹
+noremap! <buffer> <LocalLeader>#0 ⁰
+noremap! <buffer> <LocalLeader>#1 ¹
+noremap! <buffer> <LocalLeader>#2 ²
+noremap! <buffer> <LocalLeader>#3 ³
+noremap! <buffer> <LocalLeader>#4 ⁴
+noremap! <buffer> <LocalLeader>#5 ⁵
+noremap! <buffer> <LocalLeader>#6 ⁶
+noremap! <buffer> <LocalLeader>#7 ⁷
+noremap! <buffer> <LocalLeader>#8 ⁸
+noremap! <buffer> <LocalLeader>#9 ⁹
+noremap! <buffer> <LocalLeader>#+ ⁺
+noremap! <buffer> <LocalLeader>#= ⁼
+noremap! <buffer> <LocalLeader>#( ⁽
+noremap! <buffer> <LocalLeader>#) ⁾
 " Lower letters
 noremap! <buffer> <LocalLeader>t ₜ
 

ftplugin/agda.vim

@@ -25,6 +25,65 @@ endif
 " we are going to use hard-coded defaults.
 call b:AgdaMod.setup(g:nvim_agda_settings)
 
+function! LogAgda(name, text, append)
+    let agdawinnr = bufwinnr('__Agda__')
+    let prevwinnr = winnr()
+    if agdawinnr == -1
+        let eventignore_save = &eventignore
+        set eventignore=all
+
+        silent keepalt botright 8split __Agda__
+
+        let &eventignore = eventignore_save
+        setlocal noreadonly
+        setlocal buftype=nofile
+        setlocal bufhidden=hide
+        setlocal noswapfile
+        setlocal nobuflisted
+        setlocal nolist
+        setlocal nonumber
+        setlocal nowrap
+        setlocal textwidth=0
+        setlocal nocursorline
+        setlocal nocursorcolumn
+
+        if exists('+relativenumber')
+            setlocal norelativenumber
+        endif
+    else
+        let eventignore_save = &eventignore
+        set eventignore=BufEnter
+
+        execute agdawinnr . 'wincmd w'
+        let &eventignore = eventignore_save
+    endif
+
+    let lazyredraw_save = &lazyredraw
+    set lazyredraw
+    let eventignore_save = &eventignore
+    set eventignore=all
+
+    let &l:statusline = a:name
+    if a:append == 'True'
+        silent put =a:text
+    else
+        silent %delete _
+        silent 0put =a:text
+    endif
+
+    0
+
+    let &lazyredraw = lazyredraw_save
+    let &eventignore = eventignore_save
+
+    let eventignore_save = &eventignore
+    set eventignore=BufEnter
+
+    execute prevwinnr . 'wincmd w'
+    let &eventignore = eventignore_save
+endfunction
+
+
 
 " Vim commands
 command! AgdaStart :call b:AgdaMod.agda_start()
@@ -78,3 +137,4 @@ nm <buffer> <LocalLeader>b :<c-u>GoalPrev<cr>
 
 " mappings
 runtime agda-input.vim
+runtime agda-input-x11.vim