[nongnu] elpa/idris-mode f2cd31d1c5 1/6: Move test files to test/ directory

[ELPA Syncer]

branch: elpa/idris-mode
commit f2cd31d1c57f82e9914a8ec5ad16aa46d53355a6
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@gmail.com>

    Move test files to test/ directory
    
    Why:
    To better separate production code and tests
---
 .github/workflows/idris2.yml                       |   1 -
 Makefile                                           |  25 +-
 idris-tests.el                                     | 581 ---------------------
 idris-tests3.el                                    |  42 --
 test/idris-commands-test.el                        | 279 ++++++++++
 test/idris-navigate-test.el                        | 262 ++++++++++
 idris-test-utils.el => test/idris-test-utils.el    |   1 +
 test/idris-tests.el                                | 141 +++++
 idris-xref-test.el => test/idris-xref-test.el      |   0
 {test-data => test/test-data}/AddClause.idr        |   0
 {test-data => test/test-data}/AddMissing.idr       |   0
 {test-data => test/test-data}/CaseSplit.idr        |   0
 test/test-data/Empty.idr                           |   0
 {test-data => test/test-data}/GenerateDef.idr      |   0
 {test-data => test/test-data}/MakeLemma.idr        |   0
 {test-data => test/test-data}/MakeWithBlock.idr    |   0
 {test-data => test/test-data}/MetavarTest.idr      |   0
 {test-data => test/test-data}/ProofSearch.idr      |   0
 {test-data => test/test-data}/Refine.idr           |   0
 {test-data => test/test-data}/TypeAtPoint.idr      |   0
 {test-data => test/test-data}/TypeError.idr        |   0
 .../test-data}/cmdline/commandlinetest.ipkg        |   0
 .../test-data}/cmdline/src/Command/Line/Test.idr   |   0
 .../test-data}/package-test/Packaging.idr          |   0
 .../test-data}/package-test/test.ipkg              |   0
 25 files changed, 693 insertions(+), 639 deletions(-)

diff --git a/.github/workflows/idris2.yml b/.github/workflows/idris2.yml
index 838da56786..f7d83570fb 100644
--- a/.github/workflows/idris2.yml
+++ b/.github/workflows/idris2.yml
@@ -94,6 +94,5 @@ jobs:
           make clean
           make build
           make test2
-          make test3
 
 # -- [ EOF ]
diff --git a/Makefile b/Makefile
index c80e51c4bb..46994f0f13 100644
--- a/Makefile
+++ b/Makefile
@@ -46,32 +46,27 @@ OBJS =      idris-commands.elc              \
 build: getdeps $(OBJS)
 
 test: getdeps build
-       $(BATCHEMACS) -L . -l ert -l idris-tests.el -f 
ert-run-tests-batch-and-exit
+       $(BATCHEMACS) -L . -l ert -l test/idris-tests.el -f 
ert-run-tests-batch-and-exit
 
 test2: getdeps build
        $(BATCHEMACS) -L . \
                -eval '(setq idris-interpreter-path (executable-find 
"idris2"))' \
-               -l ert -l idris-tests.el -f ert-run-tests-batch-and-exit
-
-test3: getdeps build
-       $(BATCHEMACS) -L . \
-               -eval '(setq idris-interpreter-path (executable-find 
"idris2"))' \
-               -l ert -l idris-tests3.el -f ert-run-tests-batch-and-exit
+               -l ert -l test/idris-tests.el -f ert-run-tests-batch-and-exit
 
 clean:
        -${RM} -f $(OBJS)
-       -${RM} -f test-data/*ibc
-       -${RM} -rf test-data/build/
+       -${RM} -f test/test-data/*ibc
+       -${RM} -rf test/test-data/build/
        -${RM} -r docs/auto docs/*.aux docs/*.log docs/*.pdf
 getdeps:
        $(BATCHEMACS) -eval \
                "(let* \
-                   ((need-pkgs '($(NEED_PKGS))) \
-                    (want-pkgs (seq-remove #'package-installed-p need-pkgs))) \
-                 (unless (null want-pkgs) \
-                   (package-initialize) \
-                   (package-refresh-contents) \
-                   (mapcar #'package-install want-pkgs)))"
+                               ((need-pkgs '($(NEED_PKGS))) \
+                                (want-pkgs (seq-remove #'package-installed-p 
need-pkgs))) \
+                       (unless (null want-pkgs) \
+                               (package-initialize) \
+                               (package-refresh-contents) \
+                               (mapcar #'package-install want-pkgs)))"
 
 docs: docs/documentation.tex
        -@( cd docs/ && latexmk -xelatex documentation.tex )
diff --git a/idris-tests.el b/idris-tests.el
deleted file mode 100644
index 5f3476ab04..0000000000
--- a/idris-tests.el
+++ /dev/null
@@ -1,581 +0,0 @@
-;;; idris-tests.el --- Tests for idris-mode  -*- lexical-binding: t -*-
-
-;; Copyright (C) 2014  David Raymond Christiansen
-
-;; Author: David Raymond Christiansen <drc@itu.dk>
-;; Keywords: languages
-
-;; This program is free software; you can redistribute it and/or modify
-;; it under the terms of the GNU General Public License as published by
-;; the Free Software Foundation, either version 3 of the License, or
-;; (at your option) any later version.
-
-;; This program is distributed in the hope that it will be useful,
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-;; GNU General Public License for more details.
-
-;; You should have received a copy of the GNU General Public License
-;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-;;; Commentary:
-
-;; This is a collection of simple tests for idris-mode.
-
-;;; Code:
-
-(require 'idris-mode)
-(require 'idris-navigate)
-(require 'inferior-idris)
-(require 'idris-ipkg-mode)
-(require 'cl-lib)
-(require 'idris-test-utils)
-
-
-(ert-deftest trivial-test ()
-  (should t))
-
-(ert-deftest idris-test-idris-editor-port ()
-  (let ((output "Can't find import Prelude\n37072\n"))
-    (should (string-match idris-process-port-output-regexp output))
-    (should (string= "Can't find import Prelude\n" (match-string 1 output)))
-    (should (string= "37072" (match-string 2 output))))
-  (let ((output "37072\n"))
-    (should (string-match idris-process-port-output-regexp output))
-    (should (null (match-string 1 output)))
-    (should (string= "37072" (match-string 2 output)))))
-
-(ert-deftest idris-test-idris-quit ()
-  "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers."
-  (let ((before (buffer-list)))
-    (idris-repl)
-    (dotimes (_ 5) (accept-process-output nil 1))
-    (idris-quit)
-    (let* ((after (buffer-list))
-           (extra (cl-set-difference after before)))
-      (should (= (length extra) 0)))))
-
-(ert-deftest idris-test-idris-quit-logging-enabled ()
-  "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers. In particular, only *idris-events* should
-remain."
-  (let ((before (buffer-list))
-        (idris-log-events 't))
-    (idris-repl)
-    (dotimes (_ 5) (accept-process-output nil 1))
-    (idris-quit)
-    (let* ((after (buffer-list))
-           (extra (cl-set-difference after before)))
-      (should (= (length extra) 1))
-      (should (string= (buffer-name (car extra)) idris-event-buffer-name)))
-
-    ;; Cleanup
-    (kill-buffer idris-event-buffer-name)))
-
-(ert-deftest idris-test-hole-load ()
-  "Test the hole-list-on-load setting."
-  ;;; The default setting should be to show holes
-  (should idris-hole-show-on-load)
-
-  (let ((buffer (find-file "test-data/MetavarTest.idr")))
-    ;;; Check that the file was loaded
-    (should (bufferp buffer))
-
-    ;;; Check that it shows the hole list with the option turned on
-    (with-current-buffer buffer
-      (idris-load-file))
-    ;;; Allow async stuff to happen
-    (dotimes (_ 5) (accept-process-output nil 1))
-    (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
-      ;; The buffer exists and contains characters
-      (should (bufferp mv-buffer))
-      (should (> (buffer-size mv-buffer) 10)))
-    (idris-quit)
-
-    ;; Now check that it works with the setting the other way
-    (let ((idris-hole-show-on-load nil))
-      (with-current-buffer buffer
-        (idris-load-file))
-      (dotimes (_ 5) (accept-process-output nil 1))
-      (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
-        (should-not (bufferp mv-buffer))
-        (should (null mv-buffer))))
-    ;; Clean up
-    (kill-buffer))
-
-  ;; More cleanup
-  (idris-quit))
-
-(ert-deftest idris-list-holes ()
-  "Test `idris-list-holes' command."
-  (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
-        (other-buffer (find-file-noselect "test-data/MakeWithBlock.idr")))
-    ;; Test that hole info is present without need to load file manually
-    (with-current-buffer buffer
-      (idris-list-holes)
-      (dotimes (_ 5) (accept-process-output nil 1))
-      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
-        (should (bufferp holes-buffer))
-        (should (> (buffer-size holes-buffer) 10))))
-    ;; Test that the hole info is updated for the other current buffer
-    (with-current-buffer other-buffer
-      (idris-list-holes)
-      (dotimes (_ 5) (accept-process-output nil 1))
-      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
-        (should (not (bufferp holes-buffer)))))
-
-    (kill-buffer buffer)
-    (kill-buffer other-buffer)
-    (idris-quit)))
-
-(ert-deftest idris-test-proof-search ()
-  "Test that proof search works"
-  :expected-result (if (string-match-p "idris2" idris-interpreter-path)
-                       :failed
-                     :passed)
-  (unwind-protect
-      (let ((buffer (find-file "test-data/ProofSearch.idr")))
-        (with-current-buffer buffer
-          (idris-load-file)
-          (dotimes (_ 5) (accept-process-output nil 1))
-          (goto-char (point-min))
-          (re-search-forward "search_here")
-          (goto-char (match-beginning 0))
-          (idris-proof-search)
-          (dotimes (_ 5) (accept-process-output nil 1))
-          (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc 
lteZero))))"))
-          (move-beginning-of-line nil)
-          (delete-region (point) (line-end-position))
-          (insert "prf = ?search_here")
-          (save-buffer)
-          (kill-buffer)))
-
-    ;; More cleanup
-    (idris-quit)))
-
-(ert-deftest idris-test-find-cmdline-args ()
-  "Test that idris-mode calculates command line arguments from .ipkg files."
-  ;; Outside of a project, none are found
-  (let ((buffer (find-file "test-data/ProofSearch.idr")))
-    (with-current-buffer buffer
-      (should (null (idris-ipkg-flags-for-current-buffer)))
-      (kill-buffer)))
-  ;; Inside of a project, the correct ones are found
-  (let ((buffer (find-file "test-data/cmdline/src/Command/Line/Test.idr")))
-    (with-current-buffer buffer
-      (should (equal (idris-ipkg-flags-for-current-buffer)
-                     (list "-p" "effects")))
-      (kill-buffer))))
-
-(ert-deftest idris-test-error-buffer ()
-  "Test that loading a type-incorrect Idris buffer results in an error message 
buffer."
-  (let ((buffer (find-file "test-data/TypeError.idr")))
-    (with-current-buffer buffer
-      (idris-load-file)
-      (dotimes (_ 5) (accept-process-output nil 1))
-      (should (get-buffer idris-notes-buffer-name)))
-    (with-current-buffer (get-buffer idris-notes-buffer-name)
-      (goto-char (point-min))
-      (should (re-search-forward "Nat" nil t))) ;; check that the buffer has 
something error-like
-    (with-current-buffer buffer
-      (kill-buffer))
-    (idris-quit)))
-
-(ert-deftest idris-test-idris-type-search ()
-  "Test that `idris-type-search' produces output in Idris info buffer."
-  (idris-run)
-  (funcall-interactively 'idris-type-search "Nat")
-  (with-current-buffer (get-buffer idris-info-buffer-name)
-    (goto-char (point-min))
-    (should (re-search-forward "Zero" nil t)))
-  (idris-quit))
-
-(ert-deftest idris-test-ipkg-packages-with-underscores-and-dashes ()
-  "Test that loading an ipkg file can have dependencies on packages with _ or 
- in the name."
-  (let ((buffer (find-file "test-data/package-test/Packaging.idr")))
-    (with-current-buffer buffer
-      (should (equal '("-p" "idris-free" "-p" "recursion_schemes")
-                     (idris-ipkg-pkgs-flags-for-current-buffer)))
-      (kill-buffer buffer))
-    (idris-quit)))
-
-(ert-deftest idris-test-idris-add-clause ()
-  "Test that `idris-add-clause' generates definition with hole."
-  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
-        (buffer-content (with-temp-buffer
-                          (insert-file-contents "test-data/AddClause.idr")
-                          (buffer-string))))
-    (with-current-buffer buffer
-      (goto-char (point-min))
-      (re-search-forward "test :")
-      (goto-char (match-beginning 0))
-      (funcall-interactively 'idris-add-clause nil)
-      (should (looking-at-p "test \\w+ = \\?test_rhs"))
-      (idris-delete-ibc t)
-
-      (re-search-forward "(-) :")
-      (goto-char (1+ (match-beginning 0)))
-      (funcall-interactively 'idris-add-clause nil)
-      (should (looking-at-p "(-) = \\?\\w+_rhs"))
-      (idris-delete-ibc t)
-
-      ;; Test that response with indentation (Idris2) are aligned correctly
-      ;; Idris1 response: "revAcc xs ys = ?revAcc_rhs"
-      ;; Idris2 response: "  revAcc xs ys = ?revAcc_rhs"
-      (goto-char (point-max))
-      (insert "
-myReverse : List a -> List a
-myReverse xs = revAcc [] xs where
-  revAcc : List a -> List a -> List a")
-      (search-backward "evAcc")
-      (funcall-interactively 'idris-add-clause nil)
-      (beginning-of-line)
-      (should (looking-at-p "^  revAcc xs ys = \\?revAcc_rhs"))
-
-      ;; Cleanup
-      (erase-buffer)
-      (insert buffer-content)
-      (save-buffer)
-      (kill-buffer))
-    (idris-quit)))
-
-(ert-deftest idris-test-idris-refine ()
-  "Test that `idris-refine' works as expected."
-  (let* ((buffer (find-file "test-data/Refine.idr"))
-         (buffer-content (buffer-substring-no-properties (point-min) 
(point-max))))
-    (goto-char (point-min))
-    (search-forward "test : T")
-    (beginning-of-line)
-    (funcall-interactively 'idris-add-clause nil)
-    (should (looking-at-p "test \\w+ = \\?test_rhs"))
-    (idris-delete-ibc t)
-    (search-forward "?test")
-    (funcall-interactively 'idris-refine "x")
-    (should (looking-at-p
-             (if (>=-protocol-version 2 1)
-                 "x"
-               "?test_rhs1")))
-    (idris-delete-ibc t)
-    ;; Cleanup
-    ;; (sit-for 3) ;; usefull for manual inspection before restore
-    (erase-buffer)
-    (insert buffer-content)
-    (save-buffer)
-    (kill-buffer)
-    (idris-quit)))
-
-(ert-deftest idris-test-idris-type-at-point ()
-  "Test that `idris-type-at-point' works."
-  (let ((buffer (find-file-noselect "test-data/AddClause.idr")))
-    ;; Assert that we have clean global test state
-    (should (not idris-connection))
-    (with-current-buffer buffer
-      ;; Hack to reduce random failures
-      ;; TODO: Fix the leak
-      (idris-delete-ibc t)
-      (goto-char (point-min))
-      (re-search-forward "data Test")
-      (funcall-interactively 'idris-type-at-point nil)
-      ;; Assert that Idris connection is created
-      (should idris-connection)
-      ;; Assert that focus is in the Idris info buffer
-      (should (string= (buffer-name) idris-info-buffer-name))
-      ;; Assert that the info buffer displays a type
-      (should (string-match-p "Test : Type" (buffer-substring-no-properties 
(point-min) (point-max))))
-
-      ;; TODO: How to emulate "q" key binding to quit info buffer?
-      (idris-info-quit)
-      ;; Assert leaving info buffer will get us back to Idris code buffer
-      (should (eq (current-buffer) buffer))
-
-      ;; Cleanup
-      (kill-buffer))
-    (idris-quit)))
-
-(ert-deftest idris-test-warning-overlay ()
-  "Test that `idris-warning-overaly-point' works as expected."
-  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
-         (warning '("AddClause.idr" (5 7) (5 17) "Some warning message" ()))
-         (idris-raw-warnings '())
-         (idris-process-current-working-directory (file-name-directory 
(buffer-file-name buffer)))
-         (expected-position)
-         (expected-overlay))
-    (with-current-buffer buffer
-      (goto-char (point-min))
-      (re-search-forward "data Test")
-      (setq expected-position (point))
-
-      (idris-warning-overlay warning)
-
-      ;; Assert that the point position does not change
-      ;; https://github.com/idris-community/idris2-mode/issues/36
-      (should (eq (point) expected-position))
-
-      ;; Assert side effect
-      (should (not (null idris-raw-warnings)))
-
-      ;; Assert that overlay was added
-      (setq expected-overlay (car (overlays-in (point-min) (point-max))))
-      (should (not (null expected-overlay)))
-      (should (string= (overlay-get expected-overlay 'help-echo)
-                       "Some warning message"))
-      ;; Cleanup
-      (kill-buffer))))
-
-(ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
-  "Test idris-backard-toplevel navigation command."
-  (idris-test-with-temp-buffer
-   "interface DataStore (m : Type -> Type) where
-  data Store : Access -> Type
-
-  connect : ST m Var [add (Store LoggedOut)]
-  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
-  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
-  login : (store : Var) ->
-          ST m LoginResult [store ::: Store LoggedOut :->
-                             (\\res => Store (case res of
-                                                  OK => LoggedIn
-                                                  BadPassword => LoggedOut))]
-  logout : (store : Var) ->
-           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
-          (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
-   = do st <- call connect
-        OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               disconnect st
-                               getData failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        disconnect st
-        getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
-           (st, failcount : Var) ->
-           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
-   = do OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               getData2 st failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        getData2 st failcount"
-   (goto-char (point-max))
-   (idris-backward-toplevel)
-   (should (looking-at "getData2 st"))
-   ;; (goto-char (point-max))
-   (search-backward "Number")
-   (idris-backward-toplevel)
-   (should (looking-at "getData failcount"))
-   (search-backward "LoggedIn")
-   (idris-backward-toplevel)
-   (should (looking-at "interface DataStore"))
-   ))
-
-(ert-deftest idris-forward-toplevel-navigation-test-2pTac9 ()
-  "Test idris-forard-toplevel navigation command."
-  (idris-test-with-temp-buffer-point-min
-   "interface DataStore (m : Type -> Type) where
-  data Store : Access -> Type
-
-  connect : ST m Var [add (Store LoggedOut)]
-  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
-  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
-  login : (store : Var) ->
-          ST m LoginResult [store ::: Store LoggedOut :->
-                             (\\res => Store (case res of
-                                                  OK => LoggedIn
-                                                  BadPassword => LoggedOut))]
-  logout : (store : Var) ->
-           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
-          (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
-   = do st <- call connect
-        OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               disconnect st
-                               getData failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        disconnect st
-        getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
-           (st, failcount : Var) ->
-           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
-   = do OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               getData2 st failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        getData2 st failcount"
-   (search-forward "DataStore")
-   (idris-forward-toplevel)
-   (should (empty-line-p))
-   (skip-chars-backward " \t\r\n\f")
-   (should (looking-back "Store LoggedOut]" (line-beginning-position)))
-   (idris-forward-toplevel)
-   (should (looking-at "getData failcount"))
-   (idris-forward-toplevel)
-   (should (empty-line-p))
-   (skip-chars-backward " \t\r\n\f")
-   (should (looking-back "getData failcount" (line-beginning-position)))
-   ;; (goto-char (point-max))
-   (search-forward "Number")
-   (idris-forward-toplevel)
-   (should (looking-back "getData2 st failcount" (line-beginning-position)))
-   ))
-
-(ert-deftest idris-backard-statement-navigation-test-2pTac9 ()
-  "Test idris-backard-statement navigation command."
-  (idris-test-with-temp-buffer
-   "interface DataStore (m : Type -> Type) where
-  data Store : Access -> Type
-
-  connect : ST m Var [add (Store LoggedOut)]
-  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
-  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
-  login : (store : Var) ->
-          ST m LoginResult [store ::: Store LoggedOut :->
-                             (\\res => Store (case res of
-                                                  OK => LoggedIn
-                                                  BadPassword => LoggedOut))]
-  logout : (store : Var) ->
-           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
-          (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
-   = do st <- call connect
-        OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               disconnect st
-                               getData failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        disconnect st
-        getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
-           (st, failcount : Var) ->
-           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
-   = do OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               getData2 st failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        getData2 st failcount"
-   (goto-char (point-max))
-   (idris-backward-statement)
-   (should (looking-at "getData2 st"))
-   (search-backward "Number")
-   (idris-backward-statement)
-   (should (looking-at "putStrLn ("))
-   (idris-backward-statement)
-   (should (looking-at "write failcount"))
-   (search-backward "BadPassword")
-   (idris-backward-statement)
-   (should (looking-at "| BadPassword"))
-   (idris-backward-statement)
-   (should (looking-at "= do OK"))
-   (idris-backward-statement)
-   (should (looking-at "getData2 st"))
-   (idris-backward-statement)
-   (should (looking-at "ST m ()"))
-   ))
-
-(ert-deftest idris-forward-statement-navigation-test-2pTac9 ()
-  "Test idris-forard-statement navigation command."
-  (idris-test-with-temp-buffer-point-min
-   "interface DataStore (m : Type -> Type) where
-  data Store : Access -> Type
-
-  connect : ST m Var [add (Store LoggedOut)]
-  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
-  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
-  login : (store : Var) ->
-          ST m LoginResult [store ::: Store LoggedOut :->
-                             (\\res => Store (case res of
-                                                  OK => LoggedIn
-                                                  BadPassword => LoggedOut))]
-  logout : (store : Var) ->
-           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
-          (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
-   = do st <- call connect
-        OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               disconnect st
-                               getData failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        disconnect st
-        getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
-           (st, failcount : Var) ->
-           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
-   = do OK <- login st
-           | BadPassword => do putStrLn \"Failure\"
-                               fc <- read failcount
-                               write failcount (fc + 1)
-                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
-                               getData2 st failcount
-        secret <- readSecret st
-        putStrLn (\"Secret is: \" ++ show secret)
-        logout st
-        getData2 st failcount"
-   (search-forward "DataStore")
-   (idris-forward-statement)
-   (should (looking-back "where" (line-beginning-position)))
-   (idris-forward-statement)
-   (should (looking-back "Access -> Type" (line-beginning-position)))
-   (idris-forward-statement)
-   (should (looking-back "Store LoggedOut)]" (line-beginning-position)))
-   ))
-
-(load "idris-xref-test.el")
-(provide 'idris-tests)
-;;; idris-tests.el ends here
diff --git a/idris-tests3.el b/idris-tests3.el
deleted file mode 100644
index c03c790b91..0000000000
--- a/idris-tests3.el
+++ /dev/null
@@ -1,42 +0,0 @@
-(require 'idris-mode)
-(require 'idris-commands)
-(require 'inferior-idris)
-(require 'idris-ipkg-mode)
-(require 'cl-lib)
-(require 'idris-test-utils)
-
-
-
-;(idris-test-text-update-command "test-data/CaseSplit.idr" idris-case-split 
'(lambda (x y) 'eq))
-(ert-deftest idris-test-idris-run ()
-  (let ((buffer (find-file "test-data/Empty.idr")))
-    (should buffer)
-    (with-current-buffer buffer
-      (idris-run)
-      (dotimes (_ 5) (accept-process-output nil 0.1))
-      (should idris-process)
-      )
-    (kill-buffer))
-  (idris-quit))
-
-
-(ert-deftest idris-test-idris-connect-after-idris-run ()
-  (let ((buffer (find-file "test-data/Empty.idr")))
-    (with-current-buffer buffer
-      (idris-load-file)
-      (dotimes (_ 5) (accept-process-output nil 0.1))
-      (should idris-connection)
-    (kill-buffer)))
-  (idris-quit))
-
-(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split 
idris-test-eq-buffer)
-(idris-ert-command-action "test-data/MakeLemma.idr" idris-make-lemma 
idris-test-eq-buffer)
-(idris-ert-command-action "test-data/GenerateDef.idr" idris-generate-def 
idris-test-eq-buffer)
-(idris-ert-command-action2 "test-data/AddClause.idr"
-                         idris-add-clause
-                         idris-test-eq-buffer)
-
-
-(null nil)
-(provide 'idris-tests3)
-;;; idris-tests.el ends here
diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el
new file mode 100644
index 0000000000..b165bbf38f
--- /dev/null
+++ b/test/idris-commands-test.el
@@ -0,0 +1,279 @@
+;;; idris-commands-test.el --- Tests for interactive commands
+
+;; Keywords: languages
+
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; This is a collection of tests for interactive commands in idris-mode.
+
+;;; Code:
+
+(require 'idris-commands)
+(require 'idris-test-utils)
+
+(require 'ert)
+(require 'cl-lib)
+
+(defun normalised-buffer-list ()
+  "Buffer list without randomly appearing internal buffer(s)."
+  (cl-delete-if (lambda (b) (string-match-p "code-conversion-work" 
(buffer-name b)))
+                (buffer-list)))
+
+(ert-deftest idris-test-idris-run ()
+  (let ((buffer (find-file "test-data/Empty.idr")))
+    (should buffer)
+    (with-current-buffer buffer
+      (idris-run)
+      (dotimes (_ 5) (accept-process-output nil 0.1))
+      (should idris-process)
+      (should idris-connection))
+    (idris-delete-ibc t)
+    (kill-buffer))
+  (idris-quit))
+
+(ert-deftest idris-test-idris-quit ()
+  "Ensure that running Idris and quitting doesn't leave behind unwanted 
buffers."
+  (let ((before (normalised-buffer-list)))
+    (idris-repl)
+    (dotimes (_ 5) (accept-process-output nil 0.1))
+    (idris-quit)
+    (let* ((after (normalised-buffer-list))
+           (extra (cl-set-difference after before)))
+      (should (= (length extra) 0)))))
+
+(ert-deftest idris-test-idris-quit-logging-enabled ()
+  "Ensure that running Idris and quitting doesn't leave behind unwanted 
buffers.
+In particular, only *idris-events* should remain."
+  (let ((before (normalised-buffer-list))
+        (idris-log-events t))
+
+    (idris-repl)
+    (dotimes (_ 5) (accept-process-output nil 0.1))
+    (idris-quit)
+    (let* ((after (normalised-buffer-list))
+           (extra (cl-set-difference after before)))
+      (should (= (length extra) 1))
+      (should (string= (buffer-name (car extra)) idris-event-buffer-name)))
+
+    ;; Cleanup
+    (kill-buffer idris-event-buffer-name)))
+
+(ert-deftest idris-load-file-idris-hole-show-on-load-enabled ()
+  "Test that the holes buffer is created."
+  (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
+        (idris-hole-show-on-load t))
+    (with-current-buffer buffer
+      (idris-load-file)
+
+      ;; Allow async stuff to happen
+      (dotimes (_ 5) (accept-process-output nil 0.1))
+      (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
+        ;; The buffer exists and contains characters
+        (should (bufferp mv-buffer))
+        (should (> (buffer-size mv-buffer) 10))
+        (kill-buffer mv-buffer))
+
+      ;; Clean up
+      (with-current-buffer buffer
+        (idris-delete-ibc t)
+        (kill-buffer))))
+
+  ;; More cleanup
+  (idris-quit))
+
+(ert-deftest idris-load-file-idris-hole-show-on-load-disabled ()
+  "Test that holes buffer is not created."
+  (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
+        (idris-hole-show-on-load nil))
+    (with-current-buffer buffer
+      (idris-load-file))
+    (dotimes (_ 5) (accept-process-output nil 0.1))
+    (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
+      (should-not (bufferp mv-buffer))
+      (should (null mv-buffer)))
+
+    ;; Clean up
+    (with-current-buffer buffer
+      (idris-delete-ibc t)
+      (kill-buffer)))
+
+  ;; More cleanup
+  (idris-quit))
+
+(ert-deftest idris-list-holes ()
+  "Test `idris-list-holes' command."
+  (let ((other-buffer (find-file-noselect "test-data/MakeWithBlock.idr"))
+        (buffer (find-file-noselect "test-data/MetavarTest.idr")))
+
+    ;; Test that hole info is present without need to load file manually
+    (with-current-buffer buffer
+      (idris-list-holes)
+      (dotimes (_ 5) (accept-process-output nil 0.1))
+      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+        (should (bufferp holes-buffer))
+        (should (> (buffer-size holes-buffer) 10)))
+      (idris-delete-ibc t))
+
+    ;; Test that the hole info is updated for the other current buffer
+    (with-current-buffer other-buffer
+      (idris-list-holes)
+      (dotimes (_ 5) (accept-process-output nil 0.1))
+      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+        (should (not (bufferp holes-buffer))))
+      (idris-delete-ibc t))
+
+    (kill-buffer buffer)
+    (kill-buffer other-buffer)
+    (idris-quit)))
+
+(when (string-match-p "idris$" idris-interpreter-path)
+  (ert-deftest idris-test-proof-search ()
+    "Test that proof search works."
+    :expected-result (if (string-match-p "idris2$" idris-interpreter-path)
+                         :failed
+                       :passed)
+    (skip-unless (string-match-p "idris$" idris-interpreter-path))
+
+    (let ((buffer (find-file "test-data/ProofSearch.idr")))
+      (with-current-buffer buffer
+        (idris-load-file)
+        (dotimes (_ 5) (accept-process-output nil 0.1))
+        (goto-char (point-min))
+        (re-search-forward "search_here")
+        (goto-char (match-beginning 0))
+        (idris-proof-search)
+        (dotimes (_ 5) (accept-process-output nil 0.1))
+        (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc 
lteZero))))"))
+        (move-beginning-of-line nil)
+        (delete-region (point) (line-end-position))
+        (insert "prf = ?search_here")
+        (save-buffer)
+        (idris-delete-ibc t)
+        (kill-buffer)))
+
+    ;; More cleanup
+    (idris-quit)))
+
+(ert-deftest idris-test-idris-type-search ()
+  "Test that `idris-type-search' produces output in Idris info buffer."
+  (idris-run)
+  (funcall-interactively 'idris-type-search "Nat")
+  (with-current-buffer (get-buffer idris-info-buffer-name)
+    (goto-char (point-min))
+    (should (re-search-forward "Zero" nil t)))
+  (idris-quit))
+
+(ert-deftest idris-test-idris-add-clause ()
+  "Test that `idris-add-clause' generates definition with hole."
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+        (buffer-content (with-temp-buffer
+                          (insert-file-contents "test-data/AddClause.idr")
+                          (buffer-string))))
+    (with-current-buffer buffer
+      (goto-char (point-min))
+      (re-search-forward "test :")
+      (goto-char (match-beginning 0))
+      (funcall-interactively 'idris-add-clause nil)
+      (should (looking-at-p "test \\w+ = \\?test_rhs"))
+      (idris-delete-ibc t)
+
+      (re-search-forward "(-) :")
+      (goto-char (1+ (match-beginning 0)))
+      (funcall-interactively 'idris-add-clause nil)
+      (should (looking-at-p "(-) = \\?\\w+_rhs"))
+      (idris-delete-ibc t)
+
+      ;; Test that response with indentation (Idris2) are aligned correctly
+      ;; Idris1 response: "revAcc xs ys = ?revAcc_rhs"
+      ;; Idris2 response: "  revAcc xs ys = ?revAcc_rhs"
+      (goto-char (point-max))
+      (insert "
+myReverse : List a -> List a
+myReverse xs = revAcc [] xs where
+  revAcc : List a -> List a -> List a")
+      (search-backward "evAcc")
+      (funcall-interactively 'idris-add-clause nil)
+      (beginning-of-line)
+      (should (looking-at-p "^  revAcc xs ys = \\?revAcc_rhs"))
+
+      ;; Cleanup
+      (erase-buffer)
+      (insert buffer-content)
+      (save-buffer)
+      (kill-buffer))
+    (idris-quit)))
+
+(ert-deftest idris-test-idris-refine ()
+  "Test that `idris-refine' works as expected."
+  (let* ((buffer (find-file "test-data/Refine.idr"))
+         (buffer-content (buffer-substring-no-properties (point-min) 
(point-max))))
+    (goto-char (point-min))
+    (search-forward "test : T")
+    (beginning-of-line)
+    (funcall-interactively 'idris-add-clause nil)
+    (should (looking-at-p "test \\w+ = \\?test_rhs"))
+    (idris-delete-ibc t)
+    (search-forward "?test")
+    (funcall-interactively 'idris-refine "x")
+    (should (looking-at-p
+             (if (>=-protocol-version 2 1)
+                 "x"
+               "?test_rhs1")))
+
+    ;; Cleanup
+    (idris-delete-ibc t)
+    (erase-buffer)
+    (insert buffer-content)
+    (save-buffer)
+    (kill-buffer)
+    (idris-quit)))
+
+(ert-deftest idris-test-idris-type-at-point ()
+  "Test that `idris-type-at-point' works."
+  (let ((buffer (find-file-noselect "test-data/AddClause.idr")))
+    ;; Assert that we have clean global test state
+    (should (not idris-connection))
+    (with-current-buffer buffer
+      (goto-char (point-min))
+      (re-search-forward "data Test")
+      (funcall-interactively 'idris-type-at-point nil)
+      ;; Assert that Idris connection is created
+      (should idris-connection)
+      ;; Assert that focus is in the Idris info buffer
+      (should (string= (buffer-name) idris-info-buffer-name))
+      ;; Assert that the info buffer displays a type
+      (should (string-match-p "Test : Type" (buffer-substring-no-properties 
(point-min) (point-max))))
+
+      ;; TODO: How to emulate "q" key binding to quit info buffer?
+      (idris-info-quit)
+      ;; Assert leaving info buffer will get us back to Idris code buffer
+      (should (eq (current-buffer) buffer))
+
+      ;; Cleanup
+      (idris-delete-ibc t)
+      (kill-buffer))
+    (idris-quit)))
+
+;; Tests by Yasuhiko Watanabe
+;; https://github.com/idris-hackers/idris-mode/pull/537/files
+(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split 
idris-test-eq-buffer)
+(idris-ert-command-action "test-data/MakeLemma.idr" idris-make-lemma 
idris-test-eq-buffer)
+(when (string-match-p "idris2$" idris-interpreter-path)
+  (idris-ert-command-action "test-data/GenerateDef.idr" idris-generate-def 
idris-test-eq-buffer))
+(idris-ert-command-action2 "test-data/AddClause.idr" idris-add-clause 
idris-test-eq-buffer)
+
+(provide 'idris-commands-test)
+;;; idris-commands-test.el ends here
diff --git a/test/idris-navigate-test.el b/test/idris-navigate-test.el
new file mode 100644
index 0000000000..e0b4e5b0e9
--- /dev/null
+++ b/test/idris-navigate-test.el
@@ -0,0 +1,262 @@
+(require 'idris-navigate)
+
+;; Testing
+;; load-file-name is present in batch mode and buffer-file-name in interactive
+;; (add-to-list 'load-path
+;;              (file-name-directory (or load-file-name buffer-file-name)))
+
+(require 'ert)
+(require 'idris-test-utils)
+
+(ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
+  "Test idris-backard-toplevel navigation command."
+  (idris-test-with-temp-buffer
+   "interface DataStore (m : Type -> Type) where
+  data Store : Access -> Type
+
+  connect : ST m Var [add (Store LoggedOut)]
+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+  login : (store : Var) ->
+          ST m LoginResult [store ::: Store LoggedOut :->
+                             (\\res => Store (case res of
+                                                  OK => LoggedIn
+                                                  BadPassword => LoggedOut))]
+  logout : (store : Var) ->
+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+          (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+   = do st <- call connect
+        OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               disconnect st
+                               getData failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        disconnect st
+        getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+           (st, failcount : Var) ->
+           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+   = do OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               getData2 st failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        getData2 st failcount"
+   (goto-char (point-max))
+   (idris-backward-toplevel)
+   (should (looking-at "getData2 st"))
+   ;; (goto-char (point-max))
+   (search-backward "Number")
+   (idris-backward-toplevel)
+   (should (looking-at "getData failcount"))
+   (search-backward "LoggedIn")
+   (idris-backward-toplevel)
+   (should (looking-at "interface DataStore"))
+   ))
+
+(ert-deftest idris-forward-toplevel-navigation-test-2pTac9 ()
+  "Test idris-forard-toplevel navigation command."
+  (idris-test-with-temp-buffer-point-min
+   "interface DataStore (m : Type -> Type) where
+  data Store : Access -> Type
+
+  connect : ST m Var [add (Store LoggedOut)]
+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+  login : (store : Var) ->
+          ST m LoginResult [store ::: Store LoggedOut :->
+                             (\\res => Store (case res of
+                                                  OK => LoggedIn
+                                                  BadPassword => LoggedOut))]
+  logout : (store : Var) ->
+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+          (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+   = do st <- call connect
+        OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               disconnect st
+                               getData failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        disconnect st
+        getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+           (st, failcount : Var) ->
+           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+   = do OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               getData2 st failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        getData2 st failcount"
+   (search-forward "DataStore")
+   (idris-forward-toplevel)
+   (should (empty-line-p))
+   (skip-chars-backward " \t\r\n\f")
+   (should (looking-back "Store LoggedOut]" (line-beginning-position)))
+   (idris-forward-toplevel)
+   (should (looking-at "getData failcount"))
+   (idris-forward-toplevel)
+   (should (empty-line-p))
+   (skip-chars-backward " \t\r\n\f")
+   (should (looking-back "getData failcount" (line-beginning-position)))
+   ;; (goto-char (point-max))
+   (search-forward "Number")
+   (idris-forward-toplevel)
+   (should (looking-back "getData2 st failcount" (line-beginning-position)))
+   ))
+
+(ert-deftest idris-backard-statement-navigation-test-2pTac9 ()
+  "Test idris-backard-statement navigation command."
+  (idris-test-with-temp-buffer
+   "interface DataStore (m : Type -> Type) where
+  data Store : Access -> Type
+
+  connect : ST m Var [add (Store LoggedOut)]
+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+  login : (store : Var) ->
+          ST m LoginResult [store ::: Store LoggedOut :->
+                             (\\res => Store (case res of
+                                                  OK => LoggedIn
+                                                  BadPassword => LoggedOut))]
+  logout : (store : Var) ->
+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+          (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+   = do st <- call connect
+        OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               disconnect st
+                               getData failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        disconnect st
+        getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+           (st, failcount : Var) ->
+           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+   = do OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               getData2 st failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        getData2 st failcount"
+   (goto-char (point-max))
+   (idris-backward-statement)
+   (should (looking-at "getData2 st"))
+   (search-backward "Number")
+   (idris-backward-statement)
+   (should (looking-at "putStrLn ("))
+   (idris-backward-statement)
+   (should (looking-at "write failcount"))
+   (search-backward "BadPassword")
+   (idris-backward-statement)
+   (should (looking-at "| BadPassword"))
+   (idris-backward-statement)
+   (should (looking-at "= do OK"))
+   (idris-backward-statement)
+   (should (looking-at "getData2 st"))
+   (idris-backward-statement)
+   (should (looking-at "ST m ()"))
+   ))
+
+(ert-deftest idris-forward-statement-navigation-test-2pTac9 ()
+  "Test idris-forard-statement navigation command."
+  (idris-test-with-temp-buffer-point-min
+   "interface DataStore (m : Type -> Type) where
+  data Store : Access -> Type
+
+  connect : ST m Var [add (Store LoggedOut)]
+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+  login : (store : Var) ->
+          ST m LoginResult [store ::: Store LoggedOut :->
+                             (\\res => Store (case res of
+                                                  OK => LoggedIn
+                                                  BadPassword => LoggedOut))]
+  logout : (store : Var) ->
+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+          (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+   = do st <- call connect
+        OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               disconnect st
+                               getData failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        disconnect st
+        getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+           (st, failcount : Var) ->
+           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+   = do OK <- login st
+           | BadPassword => do putStrLn \"Failure\"
+                               fc <- read failcount
+                               write failcount (fc + 1)
+                               putStrLn (\"Number of failures: \" ++ show (fc 
+ 1))
+                               getData2 st failcount
+        secret <- readSecret st
+        putStrLn (\"Secret is: \" ++ show secret)
+        logout st
+        getData2 st failcount"
+   (search-forward "DataStore")
+   (idris-forward-statement)
+   (should (looking-back "where" (line-beginning-position)))
+   (idris-forward-statement)
+   (should (looking-back "Access -> Type" (line-beginning-position)))
+   (idris-forward-statement)
+   (should (looking-back "Store LoggedOut)]" (line-beginning-position)))
+   ))
diff --git a/idris-test-utils.el b/test/idris-test-utils.el
similarity index 99%
rename from idris-test-utils.el
rename to test/idris-test-utils.el
index 564314babb..27b099ab63 100644
--- a/idris-test-utils.el
+++ b/test/idris-test-utils.el
@@ -64,6 +64,7 @@ As this is not for a test of Idris itself, we do not care the 
results."
          (idris-test-run-goto-char (function ,test-fun))
          (let ((this-buffer (current-buffer)))
            (should (,buffer-p buffer this-buffer))))
+       (idris-delete-ibc t)
        (kill-buffer))
      (idris-quit)))
 
diff --git a/test/idris-tests.el b/test/idris-tests.el
new file mode 100644
index 0000000000..5b33b5ba6d
--- /dev/null
+++ b/test/idris-tests.el
@@ -0,0 +1,141 @@
+;;; idris-tests.el --- Tests for idris-mode  -*- lexical-binding: t -*-
+
+;; Copyright (C) 2014  David Raymond Christiansen
+
+;; Author: David Raymond Christiansen <drc@itu.dk>
+;; Keywords: languages
+
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; This is a collection of simple tests for idris-mode.
+;; Structuring:
+;; Packages modules (files) have their own corresponding test files.
+;; idris-commands.el -> idris-commands-test.el
+;; idris-navigate.el -> idris-navigate-test.el
+;; ..
+;; Tests for modules that are too small or not yet covered enough by tests
+;; can be left as part of the idris-tests.el
+;;
+;; Naming tests:
+;; `ert-deftest idris-X-Y`
+;; where X stands for function or state to be tested
+;; and Y for additional context or behaviour.
+;; Example:
+;; `ert-deftest idris-quit`
+;; `ert-deftest idris-quit-logging-enabled`
+
+;;; Code:
+
+;; Implementations
+(require 'idris-mode)
+
+;; Testing
+;; load-file-name is present in batch mode and buffer-file-name in interactive
+(let ((test-dir (file-name-directory (or load-file-name (buffer-file-name)))))
+  (add-to-list 'load-path test-dir)
+  ;; In batch mode default dir points to ../ and causing issues with saving
+  ;; Idris fixtures so we set it to the test-dir to avoid the issues.
+  (setq default-directory test-dir))
+
+(require 'ert)
+
+(ert-deftest trivial-test ()
+  (should t))
+
+(ert-deftest idris-editor-port ()
+  (let ((output "Can't find import Prelude\n37072\n"))
+    (should (string-match idris-process-port-output-regexp output))
+    (should (string= "Can't find import Prelude\n" (match-string 1 output)))
+    (should (string= "37072" (match-string 2 output))))
+  (let ((output "37072\n"))
+    (should (string-match idris-process-port-output-regexp output))
+    (should (null (match-string 1 output)))
+    (should (string= "37072" (match-string 2 output)))))
+
+(ert-deftest idris-test-find-cmdline-args ()
+  "Test that idris-mode calculates command line arguments from .ipkg files."
+  ;; Outside of a project, none are found
+  (let ((buffer (find-file "test-data/ProofSearch.idr")))
+    (with-current-buffer buffer
+      (should (null (idris-ipkg-flags-for-current-buffer)))
+      (kill-buffer)))
+  ;; Inside of a project, the correct ones are found
+  (let ((buffer (find-file "test-data/cmdline/src/Command/Line/Test.idr")))
+    (with-current-buffer buffer
+      (should (equal (idris-ipkg-flags-for-current-buffer)
+                     (list "-p" "effects")))
+      (kill-buffer))))
+
+(ert-deftest idris-test-error-buffer ()
+  "Test that loading a type-incorrect Idris buffer results in an error message 
buffer."
+  (let ((buffer (find-file "test-data/TypeError.idr")))
+    (with-current-buffer buffer
+      (idris-load-file)
+      (dotimes (_ 5) (accept-process-output nil 0.1))
+      (should (get-buffer idris-notes-buffer-name)))
+    (with-current-buffer (get-buffer idris-notes-buffer-name)
+      (goto-char (point-min))
+      (should (re-search-forward "Nat" nil t))) ;; check that the buffer has 
something error-like
+    (with-current-buffer buffer
+      (kill-buffer))
+    (idris-quit)))
+
+(ert-deftest idris-test-ipkg-packages-with-underscores-and-dashes ()
+  "Test that loading an ipkg file can have dependencies on packages with _ or 
- in the name."
+  (let ((buffer (find-file "test-data/package-test/Packaging.idr")))
+    (with-current-buffer buffer
+      (should (equal '("-p" "idris-free" "-p" "recursion_schemes")
+                     (idris-ipkg-pkgs-flags-for-current-buffer)))
+      (kill-buffer buffer))
+    (idris-quit)))
+
+(ert-deftest idris-test-warning-overlay ()
+  "Test that `idris-warning-overaly-point' works as expected."
+  (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+         (warning '("AddClause.idr" (5 7) (5 17) "Some warning message" ()))
+         (idris-raw-warnings '())
+         (idris-process-current-working-directory (file-name-directory 
(buffer-file-name buffer)))
+         (expected-position)
+         (expected-overlay))
+    (with-current-buffer buffer
+      (goto-char (point-min))
+      (re-search-forward "data Test")
+      (setq expected-position (point))
+
+      (idris-warning-overlay warning)
+
+      ;; Assert that the point position does not change
+      ;; https://github.com/idris-community/idris2-mode/issues/36
+      (should (eq (point) expected-position))
+
+      ;; Assert side effect
+      (should (not (null idris-raw-warnings)))
+
+      ;; Assert that overlay was added
+      (setq expected-overlay (car (overlays-in (point-min) (point-max))))
+      (should (not (null expected-overlay)))
+      (should (string= (overlay-get expected-overlay 'help-echo)
+                       "Some warning message"))
+      ;; Cleanup
+      (idris-delete-ibc t)
+      (kill-buffer))))
+
+(load "idris-commands-test")
+(load "idris-navigate-test")
+(load "idris-xref-test")
+
+(provide 'idris-tests)
+;;; idris-tests.el ends here
diff --git a/idris-xref-test.el b/test/idris-xref-test.el
similarity index 100%
rename from idris-xref-test.el
rename to test/idris-xref-test.el
diff --git a/test-data/AddClause.idr b/test/test-data/AddClause.idr
similarity index 100%
rename from test-data/AddClause.idr
rename to test/test-data/AddClause.idr
diff --git a/test-data/AddMissing.idr b/test/test-data/AddMissing.idr
similarity index 100%
rename from test-data/AddMissing.idr
rename to test/test-data/AddMissing.idr
diff --git a/test-data/CaseSplit.idr b/test/test-data/CaseSplit.idr
similarity index 100%
rename from test-data/CaseSplit.idr
rename to test/test-data/CaseSplit.idr
diff --git a/test/test-data/Empty.idr b/test/test-data/Empty.idr
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/test-data/GenerateDef.idr b/test/test-data/GenerateDef.idr
similarity index 100%
rename from test-data/GenerateDef.idr
rename to test/test-data/GenerateDef.idr
diff --git a/test-data/MakeLemma.idr b/test/test-data/MakeLemma.idr
similarity index 100%
rename from test-data/MakeLemma.idr
rename to test/test-data/MakeLemma.idr
diff --git a/test-data/MakeWithBlock.idr b/test/test-data/MakeWithBlock.idr
similarity index 100%
rename from test-data/MakeWithBlock.idr
rename to test/test-data/MakeWithBlock.idr
diff --git a/test-data/MetavarTest.idr b/test/test-data/MetavarTest.idr
similarity index 100%
rename from test-data/MetavarTest.idr
rename to test/test-data/MetavarTest.idr
diff --git a/test-data/ProofSearch.idr b/test/test-data/ProofSearch.idr
similarity index 100%
rename from test-data/ProofSearch.idr
rename to test/test-data/ProofSearch.idr
diff --git a/test-data/Refine.idr b/test/test-data/Refine.idr
similarity index 100%
rename from test-data/Refine.idr
rename to test/test-data/Refine.idr
diff --git a/test-data/TypeAtPoint.idr b/test/test-data/TypeAtPoint.idr
similarity index 100%
rename from test-data/TypeAtPoint.idr
rename to test/test-data/TypeAtPoint.idr
diff --git a/test-data/TypeError.idr b/test/test-data/TypeError.idr
similarity index 100%
rename from test-data/TypeError.idr
rename to test/test-data/TypeError.idr
diff --git a/test-data/cmdline/commandlinetest.ipkg 
b/test/test-data/cmdline/commandlinetest.ipkg
similarity index 100%
rename from test-data/cmdline/commandlinetest.ipkg
rename to test/test-data/cmdline/commandlinetest.ipkg
diff --git a/test-data/cmdline/src/Command/Line/Test.idr 
b/test/test-data/cmdline/src/Command/Line/Test.idr
similarity index 100%
rename from test-data/cmdline/src/Command/Line/Test.idr
rename to test/test-data/cmdline/src/Command/Line/Test.idr
diff --git a/test-data/package-test/Packaging.idr 
b/test/test-data/package-test/Packaging.idr
similarity index 100%
rename from test-data/package-test/Packaging.idr
rename to test/test-data/package-test/Packaging.idr
diff --git a/test-data/package-test/test.ipkg 
b/test/test-data/package-test/test.ipkg
similarity index 100%
rename from test-data/package-test/test.ipkg
rename to test/test-data/package-test/test.ipkg