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>
diff --git a/runtime/doc/filetype.txt b/runtime/doc/filetype.txt
index 88ec43f..8b4e25e 100644
--- a/runtime/doc/filetype.txt
+++ b/runtime/doc/filetype.txt
@@ -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 @@
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*
diff --git a/runtime/doc/indent.txt b/runtime/doc/indent.txt
index 9266f3a..8f347d7 100644
--- a/runtime/doc/indent.txt
+++ b/runtime/doc/indent.txt
@@ -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 @@
: 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*
diff --git a/runtime/doc/tags b/runtime/doc/tags
index f7ca8d2..00c131d 100644
--- a/runtime/doc/tags
+++ b/runtime/doc/tags
@@ -7333,6 +7333,8 @@
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*
diff --git a/runtime/filetype.vim b/runtime/filetype.vim
index fbccf22..59add19 100644
--- a/runtime/filetype.vim
+++ b/runtime/filetype.vim
@@ -1156,7 +1156,7 @@
" 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.)
diff --git a/runtime/ftplugin/idris2.vim b/runtime/ftplugin/idris2.vim
new file mode 100644
index 0000000..54e5ace
--- /dev/null
+++ b/runtime/ftplugin/idris2.vim
@@ -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
diff --git a/runtime/ftplugin/ipkg.vim b/runtime/ftplugin/ipkg.vim
new file mode 100644
index 0000000..70ae26e
--- /dev/null
+++ b/runtime/ftplugin/ipkg.vim
@@ -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
diff --git a/runtime/indent/idris2.vim b/runtime/indent/idris2.vim
new file mode 100644
index 0000000..d3c306e
--- /dev/null
+++ b/runtime/indent/idris2.vim
@@ -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
diff --git a/runtime/syntax/idris2.vim b/runtime/syntax/idris2.vim
new file mode 100644
index 0000000..e3e3d0d
--- /dev/null
+++ b/runtime/syntax/idris2.vim
@@ -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
diff --git a/runtime/syntax/ipkg.vim b/runtime/syntax/ipkg.vim
new file mode 100644
index 0000000..218c243
--- /dev/null
+++ b/runtime/syntax/ipkg.vim
@@ -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"
diff --git a/runtime/syntax/lidris2.vim b/runtime/syntax/lidris2.vim
new file mode 100644
index 0000000..328ffdf
--- /dev/null
+++ b/runtime/syntax/lidris2.vim
@@ -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"