diff --git a/runtime/doc/filetype.txt b/runtime/doc/filetype.txt index 88ec43f1df..8b4e25e17a 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 @@ 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* diff --git a/runtime/doc/indent.txt b/runtime/doc/indent.txt index 9266f3a408..8f347d7d94 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 @@ 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* diff --git a/runtime/doc/tags b/runtime/doc/tags index f7ca8d2e8d..00c131d800 100644 --- a/runtime/doc/tags +++ b/runtime/doc/tags @@ -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* diff --git a/runtime/filetype.vim b/runtime/filetype.vim index fbccf22991..59add19163 100644 --- a/runtime/filetype.vim +++ b/runtime/filetype.vim @@ -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.) diff --git a/runtime/ftplugin/idris2.vim b/runtime/ftplugin/idris2.vim new file mode 100644 index 0000000000..54e5acef90 --- /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 +" 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 0000000000..70ae26ec17 --- /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 +" 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 0000000000..d3c306e0a1 --- /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 +" Author: raichoo +" 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 +" +" 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 =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris2_indent_let + endif + + if prevline =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris2_indent_rewrite + endif + + if prevline !~ '\' + let s = match(prevline, '\.*\&.*\zs\') + if s > 0 + return s + endif + + let s = match(prevline, '\') + if s > 0 + return s + g:idris2_indent_if + endif + endif + + if prevline =~ '\(\\|\\|=\|[{([]\)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\\s\+\S\+.*$' + return match(prevline, '\') + g:idris2_indent_where + endif + + if prevline =~ '\\s\+\S\+.*$' + return match(prevline, '\') + g:idris2_indent_do + endif + + if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$' + return match(prevline, '=') + endif + + if prevline =~ '\\s\+([^)]*)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\\s\+.\+\\s*$' + return match(prevline, '\') + g:idris2_indent_case + endif + + if prevline =~ '^\s*\(\\|\<\(co\)\?data\>\)\s\+\S\+\s*$' + return match(prevline, '\(\\|\<\(co\)\?data\>\)') + &shiftwidth + endif + + if prevline =~ '^\s*\(\\|\\)\s*([^(]*)\s*$' + return match(prevline, '\(\\|\\)') + &shiftwidth + endif + + if prevline =~ '^\s*\\s*$' + return match(prevline, '\') + &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 0000000000..e3e3d0dcee --- /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 +" 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 0000000000..218c243983 --- /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 +" 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 0000000000..328ffdf685 --- /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 +" 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"