Skip to content

Commit

Permalink
Merge pull request #614 from keram/main-idris-info-to-help-mode
Browse files Browse the repository at this point in the history
Make `idris-info-mode` derived from `help-mode` and
  • Loading branch information
jfdm authored Feb 10, 2023
2 parents 3f529d7 + 600c8f5 commit 788f535
Show file tree
Hide file tree
Showing 4 changed files with 102 additions and 91 deletions.
109 changes: 23 additions & 86 deletions idris-info.el
Original file line number Diff line number Diff line change
Expand Up @@ -28,50 +28,14 @@
(require 'prop-menu)
(require 'idris-core)
(require 'idris-common-utils)


(defvar idris-info-history (list () nil ())
"A zipper into the history for idris-info-mode.
It is a three-element list whose first element is the history,
whose second element is the current item if applicable or NIL
otherwise, and whose third element is the future.")

(defun idris-info-history-clear ()
"Reset the history for Idris info buffers."
(setq idris-info-history (list () nil ())))

(defun idris-info-history-insert (contents)
"Insert CONTENTS into the Idris info history as the current node.
Following the behavior of Emacs help buffers, the future is deleted."
(pcase-let ((`(,past ,present ,_future) idris-info-history))
(setq idris-info-history
(if present
(list (cons present past) contents ())
(list past contents ())))))

(defun idris-info-history-back ()
"Move back in the Idris info history."
(setq idris-info-history
(pcase idris-info-history
(`((,prev . ,past) ,present ,future)
(list past prev (cons present future)))
(`(() ,present ,future) (list () present future)))))

(defun idris-info-history-forward ()
"Move forward in the Idris info history."
(setq idris-info-history
(pcase idris-info-history
(`(,past ,present (,next . ,future))
(list (cons present past) next future))
(`(,past ,present ()) (list past present ())))))
(require 'help-mode)

(defvar idris-info-buffer-name (idris-buffer-name :info)
"The name of the buffer containing Idris help information")

(defvar idris-info-mode-map
(let ((map (make-keymap)))
(suppress-keymap map) ; remove the self-inserting char commands
(define-key map (kbd "q") 'idris-info-quit)
;;; Allow buttons to be clicked with the left mouse button in info buffers
(define-key map [follow-link] 'mouse-face)
(cl-loop for keyer
Expand All @@ -82,75 +46,48 @@ Following the behavior of Emacs help buffers, the future is deleted."
map))

(easy-menu-define idris-info-mode-menu idris-info-mode-map
"Menu for the Idris info buffer"
"Menu for the Idris info buffer."
`("Idris Info"
["Show term interaction widgets" idris-add-term-widgets t]
["Close Idris info buffer" idris-info-quit t]))

(define-derived-mode idris-info-mode fundamental-mode "Idris Info"
"Major mode used for transient Idris information buffers
\\{idris-info-mode-map}
(define-derived-mode idris-info-mode help-mode "Idris Info"
"Major mode used for transient Idris information.
\\{idris-info-mode-map}
Invokes `idris-info-mode-hook'."
(setq-local prop-menu-item-functions '(idris-context-menu-items))
(set (make-local-variable 'prop-menu-item-functions) '(idris-context-menu-items)))
; if we use view-mode here, our key binding q would be shadowed.

(defun idris-info-buffer ()
"Return the Idris info buffer, creating one if there is not one.
Ensure that the buffer is in `idris-info-mode'."
"Return Idris info buffer."
(let ((buffer (get-buffer-create idris-info-buffer-name)))
(with-current-buffer buffer
(when (not (eq major-mode 'idris-info-mode))
(idris-info-mode)))
buffer))

(defun idris-info-quit ()
(interactive)
(idris-kill-buffer idris-info-buffer-name))

(defun idris-info-buffer-visible-p ()
(if (get-buffer-window idris-info-buffer-name 'visible) t nil))

(defun idris-info-show ()
"Show the Idris info buffer."
(interactive)
(with-current-buffer (idris-info-buffer)
(setq buffer-read-only t)
(pcase-let ((inhibit-read-only t)
(`(,past ,present ,future) idris-info-history))
(erase-buffer)
(when present
(insert present)
(insert "\n\n"))
(when past
(insert-button "[back]" 'action #'(lambda (_) (interactive) (idris-info-history-back) (idris-info-show))))
(when (and past future) (insert "\t"))
(when future
(insert-button "[forward]" 'action #'(lambda (_) (interactive) (idris-info-history-forward) (idris-info-show))))
(when (or past future) (newline))
(goto-char (point-min))))
(unless (idris-info-buffer-visible-p)
(pop-to-buffer (idris-info-buffer))
(message "Press q to close the Idris info buffer.")))
(defalias 'idris-info-quit #'quit-window)

(defmacro with-idris-info-buffer (&rest cmds)
"Execute `CMDS' in a fresh Idris info buffer, then display it to the user."
(declare (indent defun))
(let ((str-info (gensym "STR-INFO")))
`(let ((,str-info (with-temp-buffer
,@cmds
(buffer-string))))
(idris-info-history-insert ,str-info)
(idris-info-show))))

`(idris-show-info (with-temp-buffer ,@cmds (buffer-string))))

(defun idris-show-info (info-string &optional spans)
"Show INFO-STRING in the Idris info buffer, obliterating its previous contents."
(with-idris-info-buffer
(idris-propertize-spans (idris-repl-semantic-text-props spans)
(insert info-string)))
info-string)


"Show INFO-STRING with SPANS in the Idris info buffer."
(with-current-buffer (idris-info-buffer)
;; (help-xref-following t) ensure that current buffer -> idris-info-buffer
;; is recognised by `help-setup-xref' and `with-help-window'
;; as `help-buffer'
(let ((help-xref-following t))
(help-setup-xref (list #'idris-show-info info-string spans)
(called-interactively-p 'interactive))
(with-help-window (current-buffer)
(idris-propertize-spans (idris-repl-semantic-text-props spans)
(insert info-string)))
;; reset major-mode for idris-info-buffer
;; back from help-mode to idris-info-mode
(idris-info-buffer))))

(provide 'idris-info)
;;; idris-info.el ends here
7 changes: 2 additions & 5 deletions test/idris-commands-test.el
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,6 @@ myReverse xs = revAcc [] xs where
(7 4 ((:tt-term "AAAAAAAAAAAHAAAAAAA"))))))
(advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
(advice-add 'idris-eval :override #'idris-eval-stub)

(unwind-protect
(with-current-buffer buffer
(switch-to-buffer buffer)
Expand All @@ -273,10 +272,8 @@ myReverse xs = revAcc [] xs where
(funcall-interactively 'idris-type-at-point nil)
(should (eq file-loaded-p t))
(should (equal eval-args '((:type-of "Test"))))
(should (string= (buffer-name) idris-info-buffer-name))
(should (string-match-p "Test : Type" (buffer-substring-no-properties (point-min) (point-max))))
(idris-info-quit)
(should (eq (current-buffer) buffer)))
(with-current-buffer idris-info-buffer-name
(should (string-match-p "Test : Type" (buffer-string)))))

(advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
(advice-remove 'idris-eval #'idris-eval-stub)
Expand Down
76 changes: 76 additions & 0 deletions test/idris-info-test.el
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
;;; idris-info-test.el --- Tests related to Idris info buffer -*- lexical-binding: t -*-
;; Copyright (C) 2022 Marek L.

;; Author: Marek L <[email protected]>
;; Keywords: languages, Idris, help-mode, Ert

;; 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/>.

;;; Code:

(require 'ert)
(require 'idris-info)

(ert-deftest idris-show-info ()
"Test displaying information in `idris-info-buffer'."
(let ((info-str "Bool : Type")
(info-spans '((0 4 ((:name "Prelude.Bool.Bool")
(:implicit :False)
(:key "AQA")
(:decor :type)
(:doc-overview "Boolean Data Type")
(:type "Type")
(:namespace "Prelude.Bool")))
(7 4 ((:decor :type)
(:type "Type")
(:doc-overview "The type of types")
(:name "Type")))
(7 4 ((:tt-term "AAA"))))))

(idris-show-info info-str info-spans)

(should (window-valid-p (get-buffer-window (get-buffer idris-info-buffer-name))))

(with-current-buffer (get-buffer idris-info-buffer-name)
(should (string-match-p info-str (buffer-string))))
;; TODO: Assert styling, context menu etc.

;; Cleanup
(kill-buffer idris-info-buffer-name)))

(ert-deftest idris-info-buffer-history ()
"Test displaying information in `idris-info-buffer'."
(let ((info-str "First information")
(info-str2 "Second information"))

(idris-show-info info-str)

(with-current-buffer (get-buffer idris-info-buffer-name)
(should (string-match-p info-str (buffer-string)))
(should (not (string-match-p "back" (buffer-string))))

(idris-show-info info-str2)
(should (string-match-p info-str2 (buffer-string)))
(should (string-match-p "back" (buffer-string)))
(help-go-back)

(should (string-match-p info-str (buffer-string)))
(should (string-match-p "forward" (buffer-string))))

;; Cleanup
(kill-buffer idris-info-buffer-name)))

(provide 'idris-info-test)

;;; idris-info-test.el ends here
1 change: 1 addition & 0 deletions test/idris-tests.el
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,7 @@
(load "idris-navigate-test")
(load "idris-repl-test")
(load "idris-xref-test")
(load "idris-info-test")

(provide 'idris-tests)
;;; idris-tests.el ends here

0 comments on commit 788f535

Please sign in to comment.