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

1 files changed, 158 insertions, 0 deletions

diff --git a/doc/idris2-vim.txt b/doc/idris2-vim.txt
new file mode 100644
index 00000000..80a53cfc
--- /dev/null
+++ b/doc/idris2-vim.txt
@@ -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