From ad85563a4e81c23a3be5a1768b78efe81def1a57 Mon Sep 17 00:00:00 2001 From: Marek L Date: Fri, 10 Feb 2023 14:03:25 +0000 Subject: [PATCH 1/5] Update contributors list --- CONTRIBUTORS | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 588b65e6..5b14ec8d 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 From 97cd55d3b508fea18c8720e75f7dc635c78183fe Mon Sep 17 00:00:00 2001 From: Marek L Date: Fri, 10 Feb 2023 15:36:14 +0000 Subject: [PATCH 2/5] Update changelog with unreleased user facing changes in master branch --- CHANGES.markdown | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/CHANGES.markdown b/CHANGES.markdown index 9e74caea..1aac236d 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. From 0de45203f0cc07a4d4a1da527686bd97390be6dc Mon Sep 17 00:00:00 2001 From: Marek L Date: Fri, 10 Feb 2023 15:53:29 +0000 Subject: [PATCH 3/5] Update readme with example installation using `use-package` and minor copy/formatting changes. --- readme.markdown | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/readme.markdown b/readme.markdown index 691877f7..aff9f681 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,6 +171,27 @@ 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. +Example of installation and setup for Idris2 with `use-package` package from MELPA. + +```elisp +(use-package idris-mode + :ensure t + + :custom + (idris-interpreter-path "idris2")) +``` + +Example of installation and setup for Idris2 with `use-package` package directly from source. + +```elisp +(use-package idris-mode + :init (require 'idris-mode) + :load-path "path-to/idris-mode/root/source-code-directory/relative-to-current-file" + + :custom + (idris-interpreter-path "idris2")) +``` + ## Customization Customize various aspects of the mode using `M-x customize-group RET idris RET`. From bb4f53615968263ca652119747190b3f281ae75a Mon Sep 17 00:00:00 2001 From: Marek L Date: Fri, 10 Feb 2023 15:55:43 +0000 Subject: [PATCH 4/5] Move `Tests` section from "readme" to "contributing" guide file. --- CONTRIBUTING.md | 8 ++++++++ readme.markdown | 9 --------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ba4ae20b..d2112f67 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/readme.markdown b/readme.markdown index aff9f681..6fe3ee45 100644 --- a/readme.markdown +++ b/readme.markdown @@ -202,15 +202,6 @@ Additionally, you may want to update your Emacs configuration so that it does no All three-letter keybindings are available in versions with and without `C-` on the final key, following the convention from SLIME. -## 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. - - ## Integration with other Emacs packages ### Evil mode support (Vim compatibility) From e26adc572dbc8d30239c4935a24cb4304ff114e9 Mon Sep 17 00:00:00 2001 From: Marek L Date: Fri, 10 Feb 2023 17:28:48 +0000 Subject: [PATCH 5/5] Update readme with examples for `xref`, `flycheck` and `hs-minor-mode` --- readme.markdown | 57 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/readme.markdown b/readme.markdown index 6fe3ee45..a79e3194 100644 --- a/readme.markdown +++ b/readme.markdown @@ -283,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)))) +```