diff --git a/CHANGES.markdown b/CHANGES.markdown
index 9e74cae..1aac236 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 ba4ae20..d2112f6 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 588b65e..5b14ec8 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 691877f..a79e319 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 emacs initialization file. Alternatively, you can customize the variable `idris-interpreter-path` and provide an absolute path.
 
-## 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))))
+```