m-vim_plugins/vim-polyglot
1
0
Fork 0
mirror of https://github.com/sheerun/vim-polyglot.git synced 2025-11-08 11:33:52 -05:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add support for Idris2, closes #534 (#535)

Browse Source
This commit is contained in:
CodingCellist
2020-09-05 21:37:11 +02:00
committed by GitHub
parent b0124dc880
commit 3baafd5c33
19 changed files with 982 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
README.md
View File

@@ -7,7 +7,7 @@ A collection of language packs for Vim.
> One to rule them all, one to find them, one to bring them all and in the darkness bind them.
- It **won't affect your startup time**, as scripts are loaded only on demand\*.
- It **installs and updates 120+ times faster** than the <!--Package Count-->190<!--/Package Count--> packages it consists of.
- It **installs and updates 120+ times faster** than the <!--Package Count-->191<!--/Package Count--> packages it consists of.
- It is more secure because scripts loaded for all extensions are generated by vim-polyglot (ftdetect).
- Solid syntax and indentation support (other features skipped). Only the best language packs.
- All unnecessary files are ignored (like enormous documentation from php support).
@@ -130,6 +130,7 @@ If you need full functionality of any plugin, please use it directly with your p
- [html5](https://github.com/othree/html5.vim)
- [i3](https://github.com/mboughaba/i3config.vim)
- [icalendar](https://github.com/chutzpah/icalendar.vim)
- [idris2](https://github.com/edwinb/idris2-vim)
- [idris](https://github.com/idris-hackers/idris-vim)
- [ion](https://github.com/vmchale/ion-vim)
- [javascript-sql](https://github.com/statico/vim-javascript-sql)

5
after/ftplugin/idris2.vim Normal file
View File

@@ -0,0 +1,5 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
setlocal iskeyword+='
endif

82
after/syntax/idris2.vim Normal file
View File

@@ -0,0 +1,82 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
" This script allows for unicode concealing of certain characters
" For instance -> goes to →
"
" It needs vim >= 7.3, set nocompatible, set enc=utf-8
"
" If you want to turn this on, let g:idris_conceal = 1
if !exists('g:idris_conceal') || !has('conceal') || &enc != 'utf-8'
finish
endif
" vim: set fenc=utf-8:
syntax match idrNiceOperator "\\\ze[[:alpha:][:space:]_([]" conceal cchar=λ
syntax match idrNiceOperator "<-" conceal cchar=←
syntax match idrNiceOperator "->" conceal cchar=→
syntax match idrNiceOperator "\<sum\>" conceal cchar=∑
syntax match idrNiceOperator "\<product\>" conceal cchar=∏
syntax match idrNiceOperator "\<sqrt\>" conceal cchar=√
syntax match idrNiceOperator "\<pi\>" conceal cchar=π
syntax match idrNiceOperator "==" conceal cchar=≡
syntax match idrNiceOperator "\/=" conceal cchar=≠
let s:extraConceal = 1
let s:doubleArrow = 1
" Set this to 0 to use the more technically correct arrow from bar
" Some windows font don't support some of the characters,
" so if they are the main font, we don't load them :)
if has("win32")
let s:incompleteFont = [ 'Consolas'
\ , 'Lucida Console'
\ , 'Courier New'
\ ]
let s:mainfont = substitute( &guifont, '^\([^:,]\+\).*', '\1', '')
for s:fontName in s:incompleteFont
if s:mainfont ==? s:fontName
let s:extraConceal = 0
break
endif
endfor
endif
if s:extraConceal
syntax match idrNiceOperator "Void" conceal cchar=⊥
" Match greater than and lower than w/o messing with Kleisli composition
syntax match idrNiceOperator "<=\ze[^<]" conceal cchar=≤
syntax match idrNiceOperator ">=\ze[^>]" conceal cchar=≥
if s:doubleArrow
syntax match idrNiceOperator "=>" conceal cchar=⇒
else
syntax match idrNiceOperator "=>" conceal cchar=↦
endif
syntax match idrNiceOperator "=\zs<<" conceal cchar=«
syntax match idrNiceOperator "++" conceal cchar=⧺
syntax match idrNiceOperator "::" conceal cchar=∷
syntax match idrNiceOperator "-<" conceal cchar=↢
syntax match idrNiceOperator ">-" conceal cchar=↣
syntax match idrNiceOperator "-<<" conceal cchar=⤛
syntax match idrNiceOperator ">>-" conceal cchar=⤜
" Only replace the dot, avoid taking spaces around.
syntax match idrNiceOperator /\s\.\s/ms=s+1,me=e-1 conceal cchar=∘
syntax match idrNiceOperator "\.\." conceal cchar=‥
syntax match idrNiceOperator "`elem`" conceal cchar=∈
syntax match idrNiceOperator "`notElem`" conceal cchar=∉
endif
hi link idrNiceOperator Operator
hi! link Conceal Operator
setlocal conceallevel=2
endif

3
autoload/cargo/quickfix.vim
View File

@@ -1,7 +1,8 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'rust') == -1
function! cargo#quickfix#CmdPre() abort
if &filetype ==# 'rust' && get(b:, 'current_compiler', '') ==# 'cargo'
if &filetype ==# 'rust' && get(b:, 'current_compiler', '') ==# 'cargo' &&
\ &makeprg =~ '\V\^cargo\ \.\*'
" Preserve the current directory, and 'lcd' to the nearest Cargo file.
let b:rust_compiler_cargo_qf_has_lcd = haslocaldir()
let b:rust_compiler_cargo_qf_prev_cd = getcwd()

44
autoload/polyglot.vim
View File

@@ -212,6 +212,50 @@ func! polyglot#DetectReFiletype()
endfor
endfunc
func! polyglot#DetectIdrFiletype()
for lnum in range(1, min([line("$"), 5]))
let line = getline(lnum)
if line =~# '^\s*--.*[Ii]dris \=1'
setf idris | return
endif
if line =~# '^\s*--.*[Ii]dris \=2'
setf idris2 | return
endif
endfor
for lnum in range(1, min([line("$"), 30]))
let line = getline(lnum)
if line =~# '^pkgs =.*'
setf idris | return
endif
if line =~# '^depends =.*'
setf idris2 | return
endif
if line =~# '^%language \(TypeProviders\|ElabReflection\)'
setf idris | return
endif
if line =~# '^%language PostfixProjections'
setf idris2 | return
endif
if line =~# '^%access .*'
setf idris | return
endif
if exists("g:filetype_idr")
exe "setf " . g:filetype_idr | return
endif
endfor
setf idris2 | return
endfunc
func! polyglot#DetectLidrFiletype()
for lnum in range(1, min([line("$"), 200]))
let line = getline(lnum)
if line =~# '^>\s*--.*[Ii]dris \=1'
setf lidris | return
endif
endfor
setf lidris2 | return
endfunc
" Restore 'cpoptions'
let &cpo = s:cpo_save
unlet s:cpo_save

4
autoload/rustfmt.vim
View File

@@ -65,12 +65,12 @@ endfunction
function! s:RustfmtConfigOptions()
let l:rustfmt_toml = findfile('rustfmt.toml', expand('%:p:h') . ';')
if l:rustfmt_toml !=# ''
return '--config-path '.fnamemodify(l:rustfmt_toml, ":p")
return '--config-path '.shellescape(fnamemodify(l:rustfmt_toml, ":p"))
endif
let l:_rustfmt_toml = findfile('.rustfmt.toml', expand('%:p:h') . ';')
if l:_rustfmt_toml !=# ''
return '--config-path '.fnamemodify(l:_rustfmt_toml, ":p")
return '--config-path '.shellescape(fnamemodify(l:_rustfmt_toml, ":p"))
endif
" Default to edition 2018 in case no rustfmt.toml was found.

2
autoload/sleuth.vim
View File

@@ -103,6 +103,7 @@ let s:globs = {
\ 'i3config': '*.i3.config,*.i3config,i3.config,i3config',
\ 'icalendar': '*.ics',
\ 'idris': '*.idr,*.lidr,idris-response',
\ 'idris2': '*.idr,*.ipkg,idris-response',
\ 'ion': '*.ion',
\ 'javascript': '*.js,*._js,*.bones,*.cjs,*.es,*.es6,*.frag,*.gs,*.jake,*.jsb,*.jscad,*.jsfl,*.jsm,*.jss,*.mjs,*.njs,*.pac,*.sjs,*.ssjs,*.xsjs,*.xsjslib,Jakefile',
\ 'javascriptreact': '*.jsx',
@@ -116,6 +117,7 @@ let s:globs = {
\ 'kotlin': '*.kt,*.ktm,*.kts',
\ 'ledger': '*.ldg,*.ledger,*.journal',
\ 'less': '*.less',
\ 'lidris2': '*.lidr',
\ 'lilypond': '*.ly,*.ily',
\ 'litcoffee': '*.litcoffee,*.coffee.md',
\ 'livescript': '*.ls,*._ls,Slakefile',

158
doc/idris2-vim.txt Normal file
View File

@@ -0,0 +1,158 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
*idris2-vim.txt* Last change 2020 February 22
===============================================================================
===============================================================================
@@@@ @@@@@@@@ @@@@@@@@ @@@@ @@@@@@ @@ @@ @@@@ @@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@ @@@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@@ @@@@
@@ @@ @@ @@@@@@@@ @@ @@@@@@ @@@@@@@ @@ @@ @@ @@ @@@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@
@@@@ @@@@@@@@ @@ @@ @@@@ @@@@@@ @@@ @@@@ @@ @@
===============================================================================
CONTENTS *idris-vim-contents*
1. Features: |idris-vim-features|
2. Requirements: |idris-vim-requirements|
3. Functions: |idris-vim-functions|
4. Troubleshooting |idris-vim-troubleshooting|
5. Examples: |idris-vim-examples|
6. Information: |idris-vim-information|
===============================================================================
FEATURES *idris-vim-features*
* Syntax Highlighting
* Indentation
* Unicode Concealing
* Syntax Checking (via Syntastic(https://github.com/scrooloose/syntastic))
* Interactive Editing via the REPL
===============================================================================
REQUIREMENTS *idris-vim-requirements*
* Idris2 (https://github.com/edwinb/Idris2/)
OPTIONAL:
* Syntastic(https://github.com/scrooloose/syntastic) for syntax checking
* Vimshell(https://github.com/Shougo/vimshell.vim) for a REPL
===============================================================================
FUNCTIONS *idris-vim-functions*
All of the functions in idris-vim are essentially just calls back to the REPL,
so documentation for each of them is also available there.
IdrisDocumentation *IdrisDocumentation*
Shows internal documentation of the primitive under the cursor.
Mapped to '<LocalLeader>_h' by default.
IdrisResponseWin *IdrisResponseWin*
This opens an idris response window in a new pane.
Mapped to '<LocalLeader>_i' by default.
IdrisShowType *IdrisShowType*
This shows the type of the name under the cursor (or, if the cursor happens
to be over a metavariable, a bit more information about its context).
Mapped to '<LocalLeader>_t' by default.
IdrisReload *IdrisReload*
This reloads the file and type-checks the file in the current buffer.
Mapped to '<LocalLeader>_r' by default.
IdrisEval *IdrisEval*
This prompts for an expression and then evaluates it in the REPL, then
returns the result.
Mapped to '<LocalLeader>_e' by default.
IdrisCaseSplit *IdrisCaseSplit*
When the cursor is over a variable in a pattern match clause or case
expression, this splits the variable into all well-typed patterns.
Mapped to '<LocalLeader>_c' by default
IdrisAddClause *IdrisAddClause*
When the cursor is at a type declaration this creates a new clause for that
signature.
By default mapped to '<LocalLeader>_d' for an ordinary top-level definition,
'<LocalLeader>_b' for a typeclass instance definition, and
'<LocalLeader>_md' to add a pattern-matching proof clause.
IdrisAddMissing: *IdrisAddMissing*
When the cursor is over a function, this adds all clauses necessary to make
that function cover all inputs. This also eliminates clauses which would
lead to unification errors from appearing.
Mapped to '<LocalLeader>_m' by default
IdrisRefine: *IdrisRefine*
Refines the item the cursor is over (applies the name and fills in any
arguments which can be filled in via unification)
Mapped to '<LocalLeader>_f' by default
IdrisProofSearch: *IdrisProofSearch*
This attempts to find a value for the metavariable it was called on by
looking at the rest of the code. It can also be called with hints, which
are functions that can apply to help solve for the metavariable.
Mapped to '<LocalLeader>_o' without hints and '<LocalLeader>p' with hints by
default
IdrisMakeWith: *IdrisMakeWith*
When the cursor is over a pattern clause and this is called, it creates a
new with clause.
Mapped to '<LocalLeader>_w' by default
IdrisMakeLemma: *IdrisMakeLemma*
When the cursor is over a metavariable and this is called, it creates a new
top-level definition to solve the metavariable.
Mapped to '<LocalLeader>_l' by default
===============================================================================
TROUBLESHOOTING *idris-vim-troubleshooting*
If this isn't working for you, make sure that:
* There is an Idris REPL running
* For syntax checking, you have syntastic installed
* The plugins mappings exists and don't conflict with anything else installed
(You can use ':map' to check. There should be mappings similar to
'\h * :call IdrisShowDoc()'.)
* Vim recognizes you're in an idris file (you can use ':verb set ft' to check)
If none of this works, check to issue tracker on github and if nothing is
there create an issue with a detailed description of the problem.
===============================================================================
EXAMPLES *idris-vim-examples*
Some excellent tutorials/examples for interactive editing using the above
functions can be found at:
http://edwinb.wordpress.com/2013/10/28/interactive-idris-editing-with-vim/
and
http://www.scribd.com/doc/214031954/60/Interactive-Editing-in-Vim
===============================================================================
INFORMATION *idris-vim-information*
Author: edwinb
Repo: https://github.com/idris-hackers/idris-vim
Documentation by japesinator
===============================================================================
===============================================================================
" vim:ft=help:et:ts=2:sw=2:sts=2:norl:
endif

11
ftdetect/polyglot.vim
View File

@@ -795,9 +795,16 @@ if !has_key(s:disabled_packages, 'icalendar')
endif
if !has_key(s:disabled_packages, 'idris')
au BufNewFile,BufRead *.idr setf idris
au BufNewFile,BufRead *.lidr setf idris
au BufNewFile,BufRead idris-response setf idris
au! BufNewFile,BufRead *.idr call polyglot#DetectIdrFiletype()
au! BufNewFile,BufRead *.lidr call polyglot#DetectLidrFiletype()
endif
if !has_key(s:disabled_packages, 'idris2')
au BufNewFile,BufRead *.ipkg setf idris2
au BufNewFile,BufRead idris-response setf idris2
au! BufNewFile,BufRead *.idr call polyglot#DetectIdrFiletype()
au! BufNewFile,BufRead *.lidr call polyglot#DetectLidrFiletype()
endif
if !has_key(s:disabled_packages, 'ion')

334
ftplugin/idris2.vim Normal file
View File

@@ -0,0 +1,334 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
if bufname('%') == "idris-response"
finish
endif
if exists("b:did_ftplugin")
finish
endif
setlocal shiftwidth=2
setlocal tabstop=2
if !exists("g:idris_allow_tabchar") || g:idris_allow_tabchar == 0
setlocal expandtab
endif
setlocal comments=s1:{-,mb:-,ex:-},:\|\|\|,:--
setlocal commentstring=--%s
setlocal iskeyword+=?
setlocal wildignore+=*.ibc
let idris_response = 0
let b:did_ftplugin = 1
" Text near cursor position that needs to be passed to a command.
" Refinment of `expand(<cword>)` to accomodate differences between
" a (n)vim word and what Idris requires.
function! s:currentQueryObject()
let word = expand("<cword>")
if word =~ '^?'
" Cut off '?' that introduces a hole identifier.
let word = strpart(word, 1)
endif
return word
endfunction
function! s:IdrisCommand(...)
let idriscmd = shellescape(join(a:000))
" echo("idris2 " . expand ('%:p') . " --client " . idriscmd)
return system("idris2 --find-ipkg " . shellescape(expand('%:p')) . " --client " . idriscmd)
endfunction
function! IdrisDocFold(lineNum)
let line = getline(a:lineNum)
if line =~ "^\s*|||"
return "1"
endif
return "0"
endfunction
function! IdrisFold(lineNum)
return IdrisDocFold(a:lineNum)
endfunction
setlocal foldmethod=expr
setlocal foldexpr=IdrisFold(v:lnum)
function! IdrisResponseWin()
if (!bufexists("idris-response"))
botright 10split
badd idris-response
b idris-response
let g:idris_respwin = "active"
set buftype=nofile
wincmd k
elseif (bufexists("idris-response") && g:idris_respwin == "hidden")
botright 10split
b idris-response
let g:idris_respwin = "active"
wincmd k
endif
endfunction
function! IdrisHideResponseWin()
let g:idris_respwin = "hidden"
endfunction
function! IdrisShowResponseWin()
let g:idris_respwin = "active"
endfunction
function! IWrite(str)
if (bufexists("idris-response"))
let save_cursor = getcurpos()
b idris-response
%delete
let resp = split(a:str, '\n')
call append(1, resp)
b #
call setpos('.', save_cursor)
else
echo a:str
endif
endfunction
function! IdrisReload(q)
w
let file = expand('%:p')
let tc = system("idris2 --find-ipkg " . shellescape(file) . " --client ''")
if (! (tc is ""))
call IWrite(tc)
else
if (a:q==0)
call IWrite("Successfully reloaded " . file)
endif
endif
return tc
endfunction
function! IdrisReloadToLine(cline)
return IdrisReload(1)
"w
"let file = expand("%:p")
"let tc = s:IdrisCommand(":lto", a:cline, file)
"if (! (tc is ""))
" call IWrite(tc)
"endif
"return tc
endfunction
function! IdrisShowType()
w
let word = s:currentQueryObject()
let cline = line(".")
let ccol = col(".")
let ty = s:IdrisCommand(":t", word)
call IWrite(ty)
endfunction
function! IdrisShowDoc()
w
let word = expand("<cword>")
let ty = s:IdrisCommand(":doc", word)
call IWrite(ty)
endfunction
function! IdrisProofSearch(hint)
let view = winsaveview()
w
let cline = line(".")
let word = s:currentQueryObject()
if (a:hint==0)
let hints = ""
else
let hints = input ("Hints: ")
endif
let result = s:IdrisCommand(":ps!", cline, word, hints)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
endif
endfunction
function! IdrisGenerateDef()
let view = winsaveview()
w
let cline = line(".")
let word = s:currentQueryObject()
let result = s:IdrisCommand(":gd!", cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
endif
endfunction
function! IdrisMakeLemma()
let view = winsaveview()
w
let cline = line(".")
let word = s:currentQueryObject()
let result = s:IdrisCommand(":ml!", cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
call search(word, "b")
endif
endfunction
function! IdrisRefine()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let name = input ("Name: ")
let result = s:IdrisCommand(":ref!", cline, word, name)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
endif
endfunction
function! IdrisAddMissing()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let result = s:IdrisCommand(":am!", cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
endif
endfunction
function! IdrisCaseSplit()
w
let view = winsaveview()
let cline = line(".")
let ccol = col(".")
let word = expand("<cword>")
let result = s:IdrisCommand(":cs!", cline, ccol, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
endif
endfunction
function! IdrisMakeWith()
let view = winsaveview()
w
let cline = line(".")
let word = s:currentQueryObject()
let tc = IdrisReload(1)
let result = s:IdrisCommand(":mw!", cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
call search("_")
endif
endfunction
function! IdrisMakeCase()
let view = winsaveview()
w
let cline = line(".")
let word = s:currentQueryObject()
let result = s:IdrisCommand(":mc!", cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
call search("_")
endif
endfunction
function! IdrisAddClause(proof)
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
if (a:proof==0)
let fn = ":ac!"
else
let fn = ":apc!"
endif
let result = s:IdrisCommand(fn, cline, word)
if (! (result is ""))
call IWrite(result)
else
e
call winrestview(view)
call search(word)
endif
endfunction
function! IdrisEval()
w
let expr = input ("Expression: ")
let result = s:IdrisCommand(expr)
call IWrite(" = " . result)
endfunction
nnoremap <buffer> <silent> <LocalLeader>t :call IdrisShowType()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>a 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>d 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>b 0:call IdrisAddClause(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>m :call IdrisAddMissing()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>md 0:call search(":")<ENTER>b:call IdrisAddClause(1)<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>s :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>g :call IdrisGenerateDef()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>p :call IdrisProofSearch(1)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>l :call IdrisMakeLemma()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>i 0:call IdrisResponseWin()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>h :call IdrisShowDoc()<ENTER>
menu Idris.Reload <LocalLeader>r
menu Idris.Show\ Type <LocalLeader>t
menu Idris.Evaluate <LocalLeader>e
menu Idris.-SEP0- :
menu Idris.Add\ Clause <LocalLeader>a
menu Idris.Generate\ Definition <LocalLeader>g
menu Idris.Add\ with <LocalLeader>w
menu Idris.Case\ Split <LocalLeader>c
menu Idris.Add\ missing\ cases <LocalLeader>m
menu Idris.Proof\ Search <LocalLeader>s
menu Idris.Proof\ Search\ with\ hints <LocalLeader>p
au BufHidden idris-response call IdrisHideResponseWin()
au BufEnter idris-response call IdrisShowResponseWin()
endif

30
heuristics.yaml
View File

@@ -63,3 +63,33 @@ rules:
- pattern: '^\s*#(?:(?:if|ifdef|define|pragma)\s+\w|\s*include\s+[<"]|template\s*<)'
filetype: cpp
- filetype: reason
---
extensions: [idr]
rules:
- lines: 5
rules:
- pattern: '^\s*--.*[Ii]dris ?1'
filetype: idris
- pattern: '^\s*--.*[Ii]dris ?2'
filetype: idris2
- lines: 30
rules:
- pattern: '^pkgs =.*'
filetype: idris
- pattern: '^depends =.*'
filetype: idris2
- pattern: '^%language (TypeProviders|ElabReflection)'
filetype: idris
- pattern: '^%language PostfixProjections'
filetype: idris2
- pattern: '^%access .*'
filetype: idris
- override: 'g:filetype_idr'
- filetype: idris2
---
extensions: [lidr]
rules:
- lines: 200
pattern: '^>\s*--.*[Ii]dris ?1'
filetype: lidris
- filetype: lidris2

148
indent/idris2.vim Normal file
View File

@@ -0,0 +1,148 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
" indentation for idris (idris-lang.org)
"
" Based on haskell indentation by motemen <motemen@gmail.com>
"
" author: raichoo (raichoo@googlemail.com)
"
" Modify g:idris_indent_if and g:idris_indent_case to
" change indentation for `if'(default 3) and `case'(default 5).
" Example (in .vimrc):
" > let g:idris_indent_if = 2
if exists('b:did_indent')
finish
endif
let b:did_indent = 1
if !exists('g:idris_indent_if')
" if bool
" >>>then ...
" >>>else ...
let g:idris_indent_if = 3
endif
if !exists('g:idris_indent_case')
" case xs of
" >>>>>[] => ...
" >>>>>(y::ys) => ...
let g:idris_indent_case = 5
endif
if !exists('g:idris_indent_let')
" let x : Nat = O in
" >>>>x
let g:idris_indent_let = 4
endif
if !exists('g:idris_indent_rewrite')
" rewrite prf in expr
" >>>>>>>>x
let g:idris_indent_rewrite = 8
endif
if !exists('g:idris_indent_where')
" where f : Nat -> Nat
" >>>>>>f x = x
let g:idris_indent_where = 6
endif
if !exists('g:idris_indent_do')
" do x <- a
" >>>y <- b
let g:idris_indent_do = 3
endif
setlocal indentexpr=GetIdrisIndent()
setlocal indentkeys=!^F,o,O,}
function! GetIdrisIndent()
let prevline = getline(v:lnum - 1)
if prevline =~ '\s\+(\s*.\+\s\+:\s\+.\+\s*)\s\+->\s*$'
return match(prevline, '(')
elseif prevline =~ '\s\+{\s*.\+\s\+:\s\+.\+\s*}\s\+->\s*$'
return match(prevline, '{')
endif
if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$'
let s = match(prevline, '[:=]')
if s > 0
return s + 2
else
return match(prevline, '\S')
endif
endif
if prevline =~ '[{([][^})\]]\+$'
return match(prevline, '[{([]')
endif
if prevline =~ '\<let\>\s\+.\+\<in\>\s*$'
return match(prevline, '\<let\>') + g:idris_indent_let
endif
if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
return match(prevline, '\<rewrite\>') + g:idris_indent_rewrite
endif
if prevline !~ '\<else\>'
let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
if s > 0
return s
endif
let s = match(prevline, '\<if\>')
if s > 0
return s + g:idris_indent_if
endif
endif
if prevline =~ '\(\<where\>\|\<do\>\|=\|[{([]\)\s*$'
return match(prevline, '\S') + &shiftwidth
endif
if prevline =~ '\<where\>\s\+\S\+.*$'
return match(prevline, '\<where\>') + g:idris_indent_where
endif
if prevline =~ '\<do\>\s\+\S\+.*$'
return match(prevline, '\<do\>') + g:idris_indent_do
endif
if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$'
return match(prevline, '=')
endif
if prevline =~ '\<with\>\s\+([^)]*)\s*$'
return match(prevline, '\S') + &shiftwidth
endif
if prevline =~ '\<case\>\s\+.\+\<of\>\s*$'
return match(prevline, '\<case\>') + g:idris_indent_case
endif
if prevline =~ '^\s*\(\<namespace\>\|\<\(co\)\?data\>\)\s\+\S\+\s*$'
return match(prevline, '\(\<namespace\>\|\<\(co\)\?data\>\)') + &shiftwidth
endif
if prevline =~ '^\s*\(\<using\>\|\<parameters\>\)\s*([^(]*)\s*$'
return match(prevline, '\(\<using\>\|\<parameters\>\)') + &shiftwidth
endif
if prevline =~ '^\s*\<mutual\>\s*$'
return match(prevline, '\<mutual\>') + &shiftwidth
endif
let line = getline(v:lnum)
if (line =~ '^\s*}\s*' && prevline !~ '^\s*;')
return match(prevline, '\S') - &shiftwidth
endif
return match(prevline, '\S')
endfunction
endif

13
packages.yaml
View File

@@ -755,6 +755,19 @@ filetypes:
extra_filenames:
- idris-response
---
name: idris2
remote: edwinb/idris2-vim
filetypes:
- name: idris2
extensions:
- idr
- ipkg
filenames:
- idris-response
- name: lidris2
extensions:
- lidr
---
name: ion
remote: vmchale/ion-vim
filetypes:

6
scripts/build
View File

@@ -77,6 +77,12 @@ def load_data()
filetype["extensions"] ||= []
filetype["filenames"] ||= []
filetype["interpreters"] ||= []
filetype.keys.each do |key|
if key.start_with?("extra_")
raise "[#{filetype["name"]}]: #{key} is not allowed if linguist is not used"
end
end
end
end
end

30
scripts/test_extensions.vim
View File

@@ -190,6 +190,11 @@ call TestExtension('yaml.ansible', 'requirements.yaml', '')
call TestExtension('ps1xml', 'foobar.ps1xml', '')
call TestExtension('terraform', 'terraform.tf', '')
call TestExtension('idris2', 'foobar.idr', '')
call TestExtension('idris', 'foobar.idr', "pkgs : List String\npkgs = [\"NCurses\", \"Readline\"]")
let g:filetype_idr = 'fizfuz'
call TestExtension('fizfuz', 'fizfuz.idr', '')
" .m extension
call TestExtension('octave', 'matlab.m', '')
call TestExtension('objc', 'objc.m', "\n\n #import <Foundation/Foundation.h>")
@@ -215,3 +220,28 @@ call TestExtension('cpp', 'cpp.re', '#include "config.h"')
call TestExtension('cpp', 'cpp2.re', '#ifdef HAVE_CONFIG_H')
call TestExtension('cpp', 'cpp3.re', '#define YYCTYPE unsigned char')
call TestExtension('reason', 'react.re', 'ReasonReact.Router.push("");')
" Idris
call TestExtension('idris', 'lowercase.idr', '--idris1')
call TestExtension('idris', 'uppercase.idr', '--Idris1')
call TestExtension('idris', 'start-space-l.idr', '-- idris1')
call TestExtension('idris', 'start-space-u.idr', '-- Idris1')
call TestExtension('idris', 'two-spaces-l.idr', '-- idris 1')
call TestExtension('idris', 'two-spaces-u.idr', '-- Idris 1')
"call TestExtension('idris', 'mypkg.ipkg', 'package mypkg\n\npkgs = pruviloj, lightyear')
call TestExtension('idris', 'use-type-prov.idr', '%language TypeProviders')
call TestExtension('idris', 'use-elab-refl.idr', '%language ElabReflection')
call TestExtension('idris', 'access-modifier.idr', '%access export\n\npublic export\nMyTest : Type-> Type\n\nfact : Nat -> Nat')
call TestExtension('idris2', 'lowercase.idr', '--idris2')
call TestExtension('idris2', 'uppercase.idr', '--Idris2')
call TestExtension('idris2', 'start-space-l.idr', '-- idris2')
call TestExtension('idris2', 'start-space-u.idr', '-- Idris2')
call TestExtension('idris2', 'two-spaces-l.idr', '-- idris 2')
call TestExtension('idris2', 'two-spaces-u.idr', '-- Idris 2')
call TestExtension('idris2', 'mypkg.ipkg', 'package mypkg\n\ndepends = effects')
call TestExtension('idris2', 'use-post-proj.idr', '%language PostfixProjections')
" Literate Idris
call TestExtension('lidris', 'lidris-1.lidr', "Some test plaintext\n\n> --idris1\n> myfact : Nat -> Nat\n> myfact Z = 1\n> myfact (S k) = (S k) * myfact k\n\nMore plaintext")
call TestExtension('lidris2', 'lidris-2.lidr', "Some test plaintext\n\n> --idris2\n> myfact : Nat -> Nat\n> myfact Z = 1\n> myfact (S k) = (S k) * myfact k\n\nMore plaintext")

2
scripts/test_filetypes.vim
View File

@@ -106,6 +106,8 @@ call TestFiletype('html')
call TestFiletype('i3config')
call TestFiletype('icalendar')
call TestFiletype('idris')
call TestFiletype('idris2')
call TestFiletype('lidris2')
call TestFiletype('ion')
call TestFiletype('javascript')
call TestFiletype('flow')

85
syntax/idris2.vim Normal file
View File

@@ -0,0 +1,85 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
" syntax highlighting for Idris 2 (idris-lang.org)
"
" Heavily modified version of the haskell syntax
" highlighter to support Idris 2.
"
" author: raichoo (raichoo@googlemail.com)
if exists("b:current_syntax")
finish
endif
syn match idrisTypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+"
\ contains=idrisIdentifier,idrisOperators
syn region idrisParens matchgroup=idrisDelimiter start="(" end=")" contains=TOP,idrisTypeDecl
syn region idrisBrackets matchgroup=idrisDelimiter start="\[" end="]" contains=TOP,idrisTypeDecl
syn region idrisBlock matchgroup=idrisDelimiter start="{" end="}" contains=TOP,idrisTypeDecl
syn keyword idrisModule module namespace
syn keyword idrisImport import
syn keyword idrisStructure data record interface implementation
syn keyword idrisWhere where
syn keyword idrisVisibility public abstract private export
syn keyword idrisBlock parameters mutual using
syn keyword idrisTotality total partial covering
syn keyword idrisAnnotation auto impossible default constructor
syn keyword idrisStatement do case of rewrite with
syn keyword idrisLet let in
syn keyword idrisForall forall
syn keyword idrisDataOpt noHints uniqueSearch search external noNewtype containedin=idrisBrackets
syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
syn keyword idrisConditional if then else
syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
syn match idrisDelimiter "[,;]"
syn keyword idrisInfix prefix infix infixl infixr
syn match idrisOperators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)"
syn match idrisType "\<[A-Z][a-zA-Z0-9_']*\>"
syn keyword idrisTodo TODO FIXME XXX HACK contained
syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell
syn match idrisDocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell
syn match idrisMetaVar "?[a-z][A-Za-z0-9_']*"
syn match idrisPragma "%\(hide\|logging\|auto_lazy\|unbound_implicits\|undotted_record_projections\|amibguity_depth\|pair\|rewrite\|integerLit\|stringLit\|charLit\|name\|start\|allow_overloads\|language\|default\|transform\|hint\|global_hint\|defaulthint\|inline\|extern\|macro\|spec\|foreign\|runElab\|tcinline\)"
syn match idrisChar "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'"
syn match idrisBacktick "`[A-Za-z][A-Za-z0-9_']*`"
syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell
syn region idrisBlockComment start="{-" end="-}" contains=idrisBlockComment,idrisTodo,@Spell
syn match idrisIdentifier "[a-zA-Z][a-zA-z0-9_']*" contained
highlight def link idrisDeprecated Error
highlight def link idrisIdentifier Identifier
highlight def link idrisImport Structure
highlight def link idrisModule Structure
highlight def link idrisStructure Structure
highlight def link idrisStatement Statement
highlight def link idrisForall Structure
highlight def link idrisDataOpt Statement
highlight def link idrisDSL Statement
highlight def link idrisBlock Statement
highlight def link idrisAnnotation Statement
highlight def link idrisWhere Structure
highlight def link idrisLet Structure
highlight def link idrisTotality Statement
highlight def link idrisSyntax Statement
highlight def link idrisVisibility Statement
highlight def link idrisConditional Conditional
highlight def link idrisPragma Statement
highlight def link idrisNumber Number
highlight def link idrisFloat Float
highlight def link idrisDelimiter Delimiter
highlight def link idrisInfix PreProc
highlight def link idrisOperators Operator
highlight def link idrisType Include
highlight def link idrisDocComment Comment
highlight def link idrisLineComment Comment
highlight def link idrisBlockComment Comment
highlight def link idrisTodo Todo
highlight def link idrisMetaVar Macro
highlight def link idrisString String
highlight def link idrisChar String
highlight def link idrisBacktick Operator
let b:current_syntax = "idris2"
endif

26
syntax/lidris2.vim Normal file
View File

@@ -0,0 +1,26 @@
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris2') == -1
" Vim syntax file
" Language: Literate Idris 2
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim)
" Last Change: 2020 May 19
" Version: 0.1
"
" This is just a minimal adaption of the Literate Haskell syntax file.
" Read Idris highlighting.
if version < 600
syntax include @idrisTop <sfile>:p:h/idris2.vim
else
syntax include @idrisTop syntax/idris2.vim
endif
" Recognize blocks of Bird tracks, highlight as Idris.
syntax region lidrisBirdTrackBlock start="^>" end="\%(^[^>]\)\@=" contains=@idrisTop,lidrisBirdTrack
syntax match lidrisBirdTrack "^>" contained
hi def link lidrisBirdTrack Comment
let b:current_syntax = "lidris2"
endif

3
syntax/rust.vim
View File

@@ -67,10 +67,11 @@ syn match rustExternCrateString /".*"\_s*as/ contained nextgroup=rustIdentifie
syn keyword rustObsoleteExternMod mod contained nextgroup=rustIdentifier skipwhite skipempty
syn match rustIdentifier contains=rustIdentifierPrime "\%([^[:cntrl:][:space:][:punct:][:digit:]]\|_\)\%([^[:cntrl:][:punct:][:space:]]\|_\)*" display contained
syn match rustFuncName "\%([^[:cntrl:][:space:][:punct:][:digit:]]\|_\)\%([^[:cntrl:][:punct:][:space:]]\|_\)*" display contained
syn match rustFuncName "\%(r#\)\=\%([^[:cntrl:][:space:][:punct:][:digit:]]\|_\)\%([^[:cntrl:][:punct:][:space:]]\|_\)*" display contained
syn region rustMacroRepeat matchgroup=rustMacroRepeatDelimiters start="$(" end="),\=[*+]" contains=TOP
syn match rustMacroVariable "$\w\+"
syn match rustRawIdent "\<r#\h\w*" contains=NONE
" Reserved (but not yet used) keywords {{{2
syn keyword rustReservedKeyword become do priv typeof unsized abstract virtual final override