runtime(idris2): include filetype,indent+syntax plugins for (L)Idris2 + ipkg

closes: #15993

Co-authored-by: Christian Clason <ch.clason+github@icloud.com>
Signed-off-by: Serhii Khoma <srghma@gmail.com>
Signed-off-by: Christian Brabandt <cb@256bit.org>
This commit is contained in:
Serhii Khoma
2024-11-12 21:49:42 +01:00
committed by Christian Brabandt
parent f18987caa5
commit 5ca8f223f0
10 changed files with 463 additions and 3 deletions

View File

@ -1,4 +1,4 @@
*filetype.txt* For Vim version 9.1. Last change: 2024 Nov 09
*filetype.txt* For Vim version 9.1. Last change: 2024 Nov 12
VIM REFERENCE MANUAL by Bram Moolenaar
@ -667,6 +667,19 @@ HARE *ft-hare*
Since the text for this plugin is rather long it has been put in a separate
file: |ft_hare.txt|.
IDRIS2 *ft-idris2-plugin*
By default the following options are set: >
setlocal shiftwidth=2 tabstop=2 expandtab
setlocal comments=s1:{-,mb:-,ex:-},:\|\|\|,:--
setlocal commentstring=--\ %s
setlocal wildignore+=*.ibc
To use tabs instead of spaces for indentation, set the following variable
in your vimrc: >
let g:idris2#allow_tabchar = 1
JAVA *ft-java-plugin*

View File

@ -1,4 +1,4 @@
*indent.txt* For Vim version 9.1. Last change: 2024 Oct 05
*indent.txt* For Vim version 9.1. Last change: 2024 Nov 12
VIM REFERENCE MANUAL by Bram Moolenaar
@ -813,6 +813,38 @@ Detail:
: GetCSSIndent() else
<!-- --> : -1
IDRIS2 *ft-idris2-indent*
Idris 2 indentation can be configured with several variables that control the
indentation level for different language constructs:
The "g:idris2_indent_if" variable controls the indentation of `then` and `else`
blocks after `if` statements. Defaults to 3.
The "g:idris2_indent_case" variable controls the indentation of patterns in
`case` expressions. Defaults to 5.
The "g:idris2_indent_let" variable controls the indentation after `let`
bindings. Defaults to 4.
The "g:idris2_indent_rewrite" variable controls the indentation after `rewrite`
expressions. Defaults to 8.
The "g:idris2_indent_where" variable controls the indentation of `where`
blocks. Defaults to 6.
The "g:idris2_indent_do" variable controls the indentation in `do` blocks.
Defaults to 3.
Example configuration: >
let g:idris2_indent_if = 2
let g:idris2_indent_case = 4
let g:idris2_indent_let = 4
let g:idris2_indent_rewrite = 8
let g:idris2_indent_where = 6
let g:idris2_indent_do = 3
<
MATLAB *ft-matlab-indent* *matlab-indent* *matlab-indenting*

View File

@ -7333,6 +7333,8 @@ ft-html-omni insert.txt /*ft-html-omni*
ft-html-syntax syntax.txt /*ft-html-syntax*
ft-htmlos-syntax syntax.txt /*ft-htmlos-syntax*
ft-ia64-syntax syntax.txt /*ft-ia64-syntax*
ft-idris2-indent indent.txt /*ft-idris2-indent*
ft-idris2-plugin filetype.txt /*ft-idris2-plugin*
ft-inform-syntax syntax.txt /*ft-inform-syntax*
ft-java-plugin filetype.txt /*ft-java-plugin*
ft-java-syntax syntax.txt /*ft-java-syntax*

View File

@ -1156,7 +1156,7 @@ au BufRead,BufNewFile usw2kagt.log\c,usw2kagt.*.log\c,*.usw2kagt.log\c setf usw2
" Ipfilter
au BufNewFile,BufRead ipf.conf,ipf6.conf,ipf.rules setf ipfilter
" Ipkg
" Ipkg for Idris 2 language
au BufNewFile,BufRead *.ipkg setf ipkg
" Informix 4GL (source - canonical, include file, I4GL+M4 preproc.)

View File

@ -0,0 +1,34 @@
" Vim ftplugin file
" Language: Idris 2
" Last Change: 2024 Nov 05
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
"
" Based on ftplugin/idris2.vim from https://github.com/edwinb/idris2-vim
if exists("b:did_ftplugin")
finish
endif
setlocal shiftwidth=2
setlocal tabstop=2
" Set g:idris2#allow_tabchar = 1 to use tabs instead of spaces
if exists('g:idris2#allow_tabchar') && g:idris2#allow_tabchar != 0
setlocal noexpandtab
else
setlocal expandtab
endif
setlocal comments=s1:{-,mb:-,ex:-},:\|\|\|,:--
setlocal commentstring=--\ %s
" makes ? a part of a word, e.g. for named holes `vzipWith f [] [] = ?vzipWith_rhs_3`, uncomment if want to reenable
" setlocal iskeyword+=?
setlocal wildignore+=*.ibc
let b:undo_ftplugin = "setlocal shiftwidth< tabstop< expandtab< comments< commentstring< iskeyword< wildignore<"
let b:did_ftplugin = 1

19
runtime/ftplugin/ipkg.vim Normal file
View File

@ -0,0 +1,19 @@
" Vim ftplugin file
" Language: Ipkg
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" Last Change: 2024 Nov 05
" Author: ShinKage
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
if exists("b:did_ftplugin")
finish
endif
setlocal comments=:--
setlocal commentstring=--\ %s
setlocal wildignore+=*.ibc
let b:undo_ftplugin = "setlocal shiftwidth< tabstop< expandtab< comments< commentstring< iskeyword< wildignore<"
let b:did_ftplugin = 1

183
runtime/indent/idris2.vim Normal file
View File

@ -0,0 +1,183 @@
" Vim indent file
" Language: Idris 2
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" Author: raichoo <raichoo@googlemail.com>
" Last Change: 2024 Nov 05
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
"
" indentation for idris (idris-lang.org)
"
" Based on haskell indentation by motemen <motemen@gmail.com>
"
" Indentation configuration variables:
"
" g:idris2_indent_if (default: 3)
" Controls indentation after 'if' statements
" Example:
" if condition
" >>>then expr
" >>>else expr
"
" g:idris2_indent_case (default: 5)
" Controls indentation of case expressions
" Example:
" case x of
" >>>>>Left y => ...
" >>>>>Right z => ...
"
" g:idris2_indent_let (default: 4)
" Controls indentation after 'let' bindings
" Example:
" let x = expr in
" >>>>body
"
" g:idris2_indent_rewrite (default: 8)
" Controls indentation after 'rewrite' expressions
" Example:
" rewrite proof in
" >>>>>>>>expr
"
" g:idris2_indent_where (default: 6)
" Controls indentation of 'where' blocks
" Example:
" function args
" >>>>>>where helper = expr
"
" g:idris2_indent_do (default: 3)
" Controls indentation in 'do' blocks
" Example:
" do x <- action
" >>>y <- action
"
" Example configuration in .vimrc:
" let g:idris2_indent_if = 2
if exists('b:did_indent')
finish
endif
setlocal indentexpr=GetIdrisIndent()
setlocal indentkeys=!^F,o,O,}
let b:did_indent = 1
let b:undo_indent = "setlocal indentexpr< indentkeys<"
" we want to use line continuations (\) BEGINNING
let s:cpo_save = &cpo
set cpo&vim
" Define defaults for indent configuration
let s:indent_defaults = {
\ 'idris2_indent_if': 3,
\ 'idris2_indent_case': 5,
\ 'idris2_indent_let': 4,
\ 'idris2_indent_rewrite': 8,
\ 'idris2_indent_where': 6,
\ 'idris2_indent_do': 3
\ }
" we want to use line continuations (\) END
let &cpo = s:cpo_save
unlet s:cpo_save
" Set up indent settings with user overrides
for [key, default] in items(s:indent_defaults)
let varname = 'g:' . key
if !exists(varname)
execute 'let' varname '=' default
endif
endfor
if exists("*GetIdrisIndent")
finish
endif
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:idris2_indent_let
endif
if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
return match(prevline, '\<rewrite\>') + g:idris2_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:idris2_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:idris2_indent_where
endif
if prevline =~ '\<do\>\s\+\S\+.*$'
return match(prevline, '\<do\>') + g:idris2_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:idris2_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
" vim:et:sw=2:sts=2

86
runtime/syntax/idris2.vim Normal file
View File

@ -0,0 +1,86 @@
" Vim syntax file
" Language: Idris 2
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" Last Change: 2024 Nov 05
" Original Author: raichoo (raichoo@googlemail.com)
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
"
if exists("b:current_syntax")
finish
endif
syn match idris2TypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+" contains=idris2Identifier,idris2Operators
syn region idris2Parens matchgroup=idris2Delimiter start="(" end=")" contains=TOP,idris2TypeDecl
syn region idris2Brackets matchgroup=idris2Delimiter start="\[" end="]" contains=TOP,idris2TypeDecl
syn region idris2Block matchgroup=idris2Delimiter start="{" end="}" contains=TOP,idris2TypeDecl
syn region idris2SnocBrackets matchgroup=idris2Delimiter start="\[<" end="]" contains=TOP
syn region idris2ListBrackets matchgroup=idris2Delimiter start="\[>" end="]" contains=TOP
syn keyword idris2Module module namespace
syn keyword idris2Import import
syn keyword idris2Structure data record interface implementation
syn keyword idris2Where where
syn keyword idris2Visibility public abstract private export
syn keyword idris2Block parameters mutual using
syn keyword idris2Totality total partial covering
syn keyword idris2Annotation auto impossible default constructor
syn keyword idris2Statement do case of rewrite with proof
syn keyword idris2Let let in
syn keyword idris2Forall forall
syn keyword idris2DataOpt noHints uniqueSearch search external noNewtype containedin=idris2Brackets
syn keyword idris2Conditional if then else
syn match idris2Number "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
syn match idris2Float "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
syn match idris2Delimiter "[,;]"
syn keyword idris2Infix prefix infix infixl infixr
syn match idris2Operators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)"
syn match idris2Type "\<[A-Z][a-zA-Z0-9_']*\>"
syn keyword idris2Todo TODO FIXME XXX HACK contained
syn match idris2LineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idris2Todo,@Spell
syn match idris2DocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idris2Todo,@Spell
syn match idris2MetaVar "?[a-zA-Z_][A-Za-z0-9_']*"
syn match idris2Pragma "%\(hide\|logging\|auto_lazy\|unbound_implicits\|prefix_record_projections\|ambiguity_depth\|nf_metavar_threshold\|search_timeout\|pair\|rewrite\|integerLit\|stringLit\|charLit\|doubleLit\|name\|start\|allow_overloads\|language\|default\|transform\|hint\|globalhint\|defaulthint\|inline\|noinline\|extern\|macro\|spec\|foreign\|nomangle\|builtin\|MkWorld\|World\|search\|runElab\|tcinline\|auto_implicit_depth\)"
syn match idris2Char "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'"
syn match idris2Backtick "`[A-Za-z][A-Za-z0-9_']*`"
syn region idris2String start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell
syn region idris2BlockComment start="{-" end="-}" contains=idris2BlockComment,idris2Todo,@Spell
syn match idris2Identifier "[a-zA-Z][a-zA-z0-9_']*" contained
" Default Highlighting {{{1
highlight def link idris2Deprecated Error
highlight def link idris2Identifier Identifier
highlight def link idris2Import Structure
highlight def link idris2Module Structure
highlight def link idris2Structure Structure
highlight def link idris2Statement Statement
highlight def link idris2Forall Structure
highlight def link idris2DataOpt Statement
highlight def link idris2DSL Statement
highlight def link idris2Block Statement
highlight def link idris2Annotation Statement
highlight def link idris2Where Structure
highlight def link idris2Let Structure
highlight def link idris2Totality Statement
highlight def link idris2Visibility Statement
highlight def link idris2Conditional Conditional
highlight def link idris2Pragma Statement
highlight def link idris2Number Number
highlight def link idris2Float Float
highlight def link idris2Delimiter Delimiter
highlight def link idris2Infix PreProc
highlight def link idris2Operators Operator
highlight def link idris2Type Include
highlight def link idris2DocComment Comment
highlight def link idris2LineComment Comment
highlight def link idris2BlockComment Comment
highlight def link idris2Todo Todo
highlight def link idris2MetaVar Macro
highlight def link idris2String String
highlight def link idris2Char String
highlight def link idris2Backtick Operator
let b:current_syntax = "idris2"
" vim: nowrap sw=2 sts=2 ts=8 noexpandtab ft=vim

66
runtime/syntax/ipkg.vim Normal file
View File

@ -0,0 +1,66 @@
" Vim syntax file
" Language: Ipkg
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" Last Change: 2020 May 19
" Version: 0.1
" Author: ShinKage
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
"
" Syntax highlight for Idris 2 Package Descriptors (idris-lang.org)
"
if exists("b:current_syntax")
finish
endif
" we want to use line continuations (\) BEGINNING
let s:cpo_save = &cpo
set cpo&vim
syn keyword ipkgKey
\ package
\ authors
\ maintainers
\ license
\ brief
\ readme
\ homepage
\ sourceloc
\ bugtracker
\ options
\ opts
\ sourcedir
\ builddir
\ outputdir
\ prebuild
\ postbuild
\ preinstall
\ postinstall
\ preclean
\ postclean
\ version
\ langversion
\ modules
\ main
\ executable
\ depends
" we want to use line continuations (\) END
let &cpo = s:cpo_save
unlet s:cpo_save
syn region ipkgString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell
syn match ipkgVersion "[0-9]*\([.][0-9]*\)*"
syn match ipkgName "[a-zA-Z][a-zA-z0-9_']*\([.][a-zA-Z][a-zA-z0-9_']*\)*" contained
syn match ipkgOperator "\(,\|&&\|<\|<=\|==\|>=\|>\)"
syn match ipkgComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=@Spell
highlight def link ipkgKey Statement
highlight def link ipkgString String
highlight def link ipkgVersion Number
highlight def link ipkgName Identifier
highlight def link ipkgOperator Operator
highlight def link ipkgComment Comment
let b:current_syntax = "ipkg"

View File

@ -0,0 +1,25 @@
" Vim syntax file
" Language: Literate Idris 2
" Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com>
" Last Change: 2020 May 19
" Version: 0.1
" License: Vim (see :h license)
" Repository: https://github.com/ShinKage/idris2-nvim
"
" This is just a minimal adaption of the Literate Haskell syntax file.
" quit when a syntax file was already loaded
if exists("b:current_syntax")
finish
endif
" Read Idris highlighting.
syntax include @idris2Top syntax/idris2.vim
" Recognize blocks of Bird tracks, highlight as Idris.
syntax region lidris2BirdTrackBlock start="^>" end="\%(^[^>]\)\@=" contains=@idris2Top,lidris2BirdTrack
syntax match lidris2BirdTrack "^>" contained
hi def link lidris2BirdTrack Comment
let b:current_syntax = "lidris2"