[nongnu] elpa/idris-mode c96f45d1b8 8/8: Merge pull request #616 from keram/changelog-update

[ELPA Syncer]

branch: elpa/idris-mode
commit c96f45d1b8fad193f09fb6139da17092003b5e74
Merge: 788f53520d e26adc572d
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #616 from keram/changelog-update
    
    [chore] Update changelog, readme and contributors files with the latest 
changes in master branch.
---
 CHANGES.markdown | 44 +++++++++++++++++++++++++-
 CONTRIBUTING.md  |  8 +++++
 CONTRIBUTORS     |  3 +-
 readme.markdown  | 95 +++++++++++++++++++++++++++++++++++++++++++++++++-------
 4 files changed, 137 insertions(+), 13 deletions(-)

diff --git a/CHANGES.markdown b/CHANGES.markdown
index 9e74caeaa2..1aac236d57 100644
--- a/CHANGES.markdown
+++ b/CHANGES.markdown
@@ -3,10 +3,52 @@
 This file documents the user-interface changes in idris-mode, starting
 with release 0.9.19.
 
+## master (unreleased)
+
+### New features
+
++ [cab781537f](https://github.com/idris-hackers/idris-mode/commit/cab781537f): 
Improved flycheck integration for Idris1 and Idris2.
++ [c9b2a4bee6](https://github.com/idris-hackers/idris-mode/commit/c9b2a4bee6): 
Xref integration to support "jump to definition" features.
++ [103f1e5fbf](https://github.com/idris-hackers/idris-mode/commit/103f1e5fbf): 
New command `M-x idris-switch-to-last-idris-buffer` to move point from Idris 
repl buffer to Idris source code buffer.
+  It is opposite of `M-x idris-switch-to-repl` and uses same key binding by 
default (`C-c C-z`).
++ [e350ed25a5](https://github.com/idris-hackers/idris-mode/commit/e350ed25a5): 
New command `idris-compile-and-execute`. Backport of 
`idris2-compile-and-execute` from 
https://github.com/idris-community/idris2-mode/pull/20/files with preserving 
backward compatibility for Idris 1.
++ [e350ed25a5](https://github.com/idris-hackers/idris-mode/commit/e350ed25a5): 
New command `idris-intro`. Backport of `idris2-intro from` 
https://github.com/idris-community/idris2-mode/pull/21/files
++ [cc098578fe](https://github.com/idris-hackers/idris-mode/commit/cc098578fe): 
Restore position after case split with improved user experience. Related to 
https://github.com/idris-hackers/idris-mode/pull/465
++ [3cce2336b7](https://github.com/idris-hackers/idris-mode/commit/3cce2336b7): 
More granular configuration for enabling semantic source highlighting.
+
+### Changes
+
++ [b6a5b2ec60](https://github.com/idris-hackers/idris-mode/commit/b6a5b2ec60): 
Kill Idris buffer and it's window if it was the only buffer in windows history.
++ [d1a9171fd7](https://github.com/idris-hackers/idris-mode/commit/d1a9171fd7): 
Jump to last Idris Code buffer when we quit buffer
++ [cd734fdc7a](https://github.com/idris-hackers/idris-mode/commit/cd734fdc7a): 
Write Idris repl history file to `~/.idris2/` directory.
++ [8329b73be8](https://github.com/idris-hackers/idris-mode/commit/8329b73be8): 
Move "words of encouragement" from mini-buffer to Idris repl banner.
++ [71ab6a35e3](https://github.com/idris-hackers/idris-mode/commit/71ab6a35e3): 
Update semantic source highlighting file only in changed code parts reducing 
buffer "flickering".
++ [e5ef933366](https://github.com/idris-hackers/idris-mode/commit/e5ef933366): 
Only display Idris repl buffer on load without moving the point.
++ [9e931bf1ff](https://github.com/idris-hackers/idris-mode/commit/9e931bf1ff): 
Make `idris-list-holes-on-load` obsolete in favour of `idris-list-holes` 
command.
++ [446c67cec7](https://github.com/idris-hackers/idris-mode/commit/446c67cec7): 
Ensure Idris connection established and current file loaded  when running 
interactive command `idris-thing-at-point`
++ [cb71c82e13](https://github.com/idris-hackers/idris-mode/commit/cb71c82e13): 
Make commands `idris-pop-to-repl` and `idris-switch-to-output-buffer` obsolete 
in favour of `idris-switch-to-repl` command.
++ [7697b8b95e](https://github.com/idris-hackers/idris-mode/commit/7697b8b95e): 
Make `idris-print-definition-of-name` obsolete in favour of 
`idris-print-definition-of-name-at-point`.
++ [600c8f584b](https://github.com/idris-hackers/idris-mode/commit/600c8f584b): 
Make Idris info buffers derived from Help mode making handling them more align 
with general Emacs conventions.
+
+### Bug fixes
+
++ [3c3a87c66c](https://github.com/idris-hackers/idris-mode/commit/3c3a87c66c): 
Fix failure to find beginning of function type definition when lifting hole and 
function name contains underscore.
++ [62c3ad2b0d](https://github.com/idris-hackers/idris-mode/commit/62c3ad2b0d): 
Do not display unnecessary `*idris-process*` buffer when loading file.
++ [486be1b740](https://github.com/idris-hackers/idris-mode/commit/486be1b740): 
Improve `idris-case-dwim` to make case expression from hole in edge case point 
positions.
++ [8ff4a2d9d5](https://github.com/idris-hackers/idris-mode/commit/8ff4a2d9d5) 
[4f654a8b20ba6](https://github.com/idris-hackers/idris-mode/commit/4f654a8b20ba6)
 [c84ed5a733](https://github.com/idris-hackers/idris-mode/commit/c84ed5a733): 
Improve resetting state on `idris-quit` making it easier to switch Idris 
version or restart connection.
++ [1382948269](https://github.com/idris-hackers/idris-mode/commit/1382948269): 
Consider `-` as operator in idris-thing-at-point . Fixes 
https://github.com/idris-community/idris2-mode/issues/16
++ [216945f4a6](https://github.com/idris-hackers/idris-mode/commit/216945f4a6): 
Fix "off-by-one" source code highlighting in Idris 1.
++ [928f785bb7](https://github.com/idris-hackers/idris-mode/commit/928f785bb7): 
Allow loading multiple files with identical name but in different directories.
++ [ac029bc67e](https://github.com/idris-hackers/idris-mode/commit/ac029bc67e): 
Remove extra white-space included by Idris2 on `idris-add-clause` command.
++ [24ce417b69](https://github.com/idris-hackers/idris-mode/commit/24ce417b69): 
Preserve point position after adding warning overlay. Resolves part of: 
https://github.com/idris-community/idris2-mode/issues/36
++ [a47811be8b](https://github.com/idris-hackers/idris-mode/commit/a47811be8b): 
Remove `{{{{{ VAL }}}}}` value from `idris-name-key` text property fixing some 
command depending on it to have meaningful or no value.
++ [3e7cbb331f](https://github.com/idris-hackers/idris-mode/commit/3e7cbb331f): 
Improve compatibility with Idris2
++ [43b6036c99](https://github.com/idris-hackers/idris-mode/commit/43b6036c99): 
Display key binding for `idris-case-split` and `idris-make-cases-from-hole` in 
menu. Resolves: https://github.com/idris-hackers/idris-mode/issues/447
+
 ## 1.1
 
 + New customisation settings:
-  + `idris-displat-words-of-encouragement` toggles showing words of 
encouragement.
+  + `idris-display-words-of-encouragement` toggles showing words of 
encouragement.
   + `idris-completion-via-compiler` toggles use of the Idris compiler to 
provide completion.
     + Tab in the repl still uses `completion-at-point`.
 + Improvements to testing harness, with support for testing against Idris2.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index ba4ae20bd8..d2112f67ad 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -7,6 +7,14 @@ Much like Idris itself, `idris-mode` is run by volunteers and 
there are no full-
 Our time is limited and we must take care to ensure that the demands of our 
day job take priority.
 Thus, we must take care in ensure that *we* can maintain `idris-mode` itself.
 
+## Tests
+
+Before sending a patch or pull request, please run the automated tests for 
`idris-mode` and correct any errors that are found. There are two kinds of test:
+
+1. The Emacs byte code compiler can catch many issues. Running `make compile` 
will invoke the byte code compiler, failing if there are any warnings. You may 
wish to run `make clean` after `make compile` to get rid of pesky `.elc` files.
+
+2. There is a test suite that can be invoked with `make test`. It requires a 
functioning `idris` executable.
+
 ## General Comments
 
 We expect contributions to come in the form of PRs (via GitHub), and larger 
discussions to take place on the project's issue tracker, the Idris Mailing 
List, or the Idris Discord.
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index 588b65e656..5b14ec8d1a 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -1,6 +1,6 @@
 # Contributors
 
-Over the years many people have contributed to the development of Idris2.
+Over the years many people have contributed to the development of idris-mode.
 We thanks the following for their contributions:
 
 Ahmad Salim Al-Sibahi
@@ -27,6 +27,7 @@ Josh
 Jozsef Hegedus
 Juergen Hoetzel
 Mario Rodas
+Marek L.
 Mark Laws
 Matti Hanninen
 Micah Werbitt
diff --git a/readme.markdown b/readme.markdown
index 691877f79d..a79e31948c 100644
--- a/readme.markdown
+++ b/readme.markdown
@@ -108,7 +108,7 @@ The following commands are available when there is an 
inferior Idris process (wh
 * `C-c C-t`: Get the type for the identifier under point. A prefix argument 
prompts for the name.
 * `C-c C-w`: Add a with block for the pattern-match clause under point
 * `C-c C-h a`: Search names, types, and docstrings for a given string.
-* `C-c C-z`: Pop to a presently open REPL buffer
+* `C-c C-z`: Pop to a presently open REPL buffer or to last Idris code buffer 
if invoked in REPL buffer.
 
 ## Online documentation
 
@@ -118,6 +118,7 @@ The Idris compiler supports documentation. The following 
commands access it:
 * `C-c C-d t`: Search for documentation regarding a particular type (`:search` 
at the REPL).
 
 Additionally, `idris-mode` integrates with `eldoc-mode`, which shows 
documentation overviews and type signatures in the minibuffer.
+(Eldoc support is yet to be implemented in the Idris2.)
 
 ## Completion
 
@@ -136,7 +137,10 @@ The following keybindings are available:
 * `C-c C-m c`: Show the core language for the term at point (`M-x 
idris-show-core-term`)
 
 ## Package files
-Idris's build system, which consists of package files ending in `.ipkg`, has 
rudimentary support from `idris-mode`. The following commands are available in 
Idris buffers or package buffers; if they are run from an Idris buffer, then 
`idris-mode` will attempt to locate the package file automatically. The 
mnemonic for `C-b` in the prefix is "build".
+
+Idris's build system, which consists of package files ending in `.ipkg`, has 
rudimentary support from `idris-mode`.
+The following commands are available in Idris buffers or package buffers; if 
they are run from an Idris buffer, then `idris-mode` will attempt to locate the 
package file automatically.
+The mnemonic for `C-b` in the prefix is "build".
 * `C-c C-b c`: Clean the package, removing `.ibc` files
 * `C-c C-b b`: Build the package
 * `C-c C-b i`: Install the package to the user's repository, building first if 
necessary
@@ -167,24 +171,36 @@ If you want `idris-mode` to be enabled by default, add 
the line `(require 'idris
 
 Idris mode is heavily dependent on the Idris compiler for its more advanced 
features. Thus, please ensure that Emacs can see your Idris binary. Emacs looks 
for executables in the directories specified in the variable `exec-path`, which 
is initialized from your PATH at startup. If Idris is not on your `PATH`, then 
you may need to add it to `exec-path` manually. E.g.: if you installed idris 
with cabal into `~/.cabal/bin`, then add the line `(add-to-list 'exec-path 
"~/.cabal/bin")` to your  [...]
 
-## Customization
+Example of installation and setup for Idris2 with `use-package` package from 
MELPA.
 
-Customize various aspects of the mode using `M-x customize-group RET idris 
RET`.
+```elisp
+(use-package idris-mode
+  :ensure t
 
-Additionally, you may want to update your Emacs configuration so that it does 
not open Idris bytecode files by default. You can do this by adding `".ibc"` to 
the variable `completion-ignored-extensions`, either in customize or by adding 
`(add-to-list 'completion-ignored-extensions ".ibc")` to your `init.el`. If you 
use `ido`, then you may also need to set `ido-ignore-extensions` to `t`.
+  :custom
+  (idris-interpreter-path "idris2"))
+```
 
-## Keybinding conventions
+Example of installation and setup for Idris2 with `use-package` package 
directly from source.
 
-All three-letter keybindings are available in versions with and without `C-` 
on the final key, following the convention from SLIME.
+```elisp
+(use-package idris-mode
+  :init (require 'idris-mode)
+  :load-path 
"path-to/idris-mode/root/source-code-directory/relative-to-current-file"
 
-## Tests
+  :custom
+  (idris-interpreter-path "idris2"))
+```
 
-Before sending a patch or pull request, please run the automated tests for 
`idris-mode` and correct any errors that are found. There are two kinds of test:
+## Customization
 
-1. The Emacs byte code compiler can catch many issues. Running `make compile` 
will invoke the byte code compiler, failing if there are any warnings. You may 
wish to run `make clean` after `make compile` to get rid of pesky `.elc` files.
+Customize various aspects of the mode using `M-x customize-group RET idris 
RET`.
 
-2. There is a test suite that can be invoked with `make test`. It requires a 
functioning `idris` executable.
+Additionally, you may want to update your Emacs configuration so that it does 
not open Idris bytecode files by default. You can do this by adding `".ibc"` to 
the variable `completion-ignored-extensions`, either in customize or by adding 
`(add-to-list 'completion-ignored-extensions ".ibc")` to your `init.el`. If you 
use `ido`, then you may also need to set `ido-ignore-extensions` to `t`.
 
+## Keybinding conventions
+
+All three-letter keybindings are available in versions with and without `C-` 
on the final key, following the convention from SLIME.
 
 ## Integration with other Emacs packages
 
@@ -267,3 +283,60 @@ Throughout a session with `idris-mode`, many frames will 
accumulate, such as `*i
 
 (add-hook 'idris-mode-hook #'my-idris-mode-hook)
 ```
+
+### Flycheck (asynchronous syntax checks in buffer)
+
+To enable on-the-fly syntax checking of Idris code using `flycheck` add these 
lines to your configuration:
+
+```elisp
+(require 'flycheck-idris)
+(add-hook 'idris-mode-hook #'flycheck-mode)
+```
+
+Example using `use-package` package:
+```elisp
+(use-package idris-mode
+  :ensure t
+
+  :config
+  (require 'flycheck-idris) ;; Syntax checker
+  (add-hook 'idris-mode-hook #'flycheck-mode))
+```
+
+### Xref (Cross-referencing commands)
+
+Jump to definitions `xref-find-definitions` (`M-.`) in current file or project 
is supported as long as Idris compiler returns file path to the definition.
+To support jump to definitions for which Idris could not find relevant source 
file you may want customise `idris-xref-idris-source-location` and 
`idris-xref-idris-source-locations`.
+You can do that interactively using `M-x customize-group` [enter] -> 
idris-xref [enter] command or
+programatically.
+Example using `use-package` package.
+
+```elisp
+(use-package idris-mode
+  :ensure t ;; Installing from (M)ELPA
+
+  :custom
+  (idris-interpreter-path "idris2")
+
+  ;; Assuming you did `git clone git@github.com:idris-lang/Idris2.git 
~/sources/idris2`
+  (idris-xref-idris-source-location "~/sources/idris2")
+  ;; Paths to random additional idris packages you may be using
+  (idris-xref-idris-source-locations '("~/sources/idris-ncurses/src"
+                                       "~/sources/idris-foo/src")))
+```
+
+### Hideshow Minor Mode (hs-minor-mode)
+
+If you have enabled hs-minor-mode globally you may want to disable it for 
Idris prover buffers
+as it may cause errors in some situations (When invoking `idris-quit` command 
for example).
+Example of enabling `hs-minor-mode` for all buffers derived from `prog-mode` 
except the
+`idris-prover` buffers.
+
+```elisp
+
+(add-hook 'prog-mode-hook
+          #'(lambda ()
+              (if (derived-mode-p 'idris-prover-script-mode)
+                  (hs-minor-mode -1)
+                (hs-minor-mode))))
+```