emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/idris-mode 0093e0b42c 13/14: Merge pull request #576 from


From: ELPA Syncer
Subject: [nongnu] elpa/idris-mode 0093e0b42c 13/14: Merge pull request #576 from keram/hole-list
Date: Thu, 1 Dec 2022 08:02:55 -0500 (EST)

branch: elpa/idris-mode
commit 0093e0b42cfeab61a7793b7c4084cb90ef360b5e
Merge: 195b432903 38f2839b58
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #576 from keram/hole-list
    
    Make hole-list buffer derived from special-mode
---
 idris-hole-list.el | 47 ++++++++++++++++++++++++-----------------------
 idris-tests.el     |  1 -
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/idris-hole-list.el b/idris-hole-list.el
index 47cd36f86d..643dbd51fa 100644
--- a/idris-hole-list.el
+++ b/idris-hole-list.el
@@ -42,7 +42,6 @@
 (defvar idris-hole-list-mode-map
   (let ((map (make-keymap)))
     (suppress-keymap map)
-    (define-key map (kbd "q") 'idris-hole-list-quit)
     (define-key map (kbd "RET") 
'idris-compiler-notes-default-action-or-show-details)
     (define-key map (kbd "<mouse-2>") 
'idris-compiler-notes-default-action-or-show-details/mouse)
     ;;; Allow buttons to be clicked with the left mouse button in the hole list
@@ -63,12 +62,16 @@
     ["Customize idris-hole-list-mode" (customize-group 'idris-hole-list) t]
     ["Customize fonts and colors" (customize-group 'idris-faces) t]))
 
-(define-derived-mode idris-hole-list-mode fundamental-mode "Idris Holes"
-  "Major mode used for transient Idris hole list buffers
-   \\{idris-hole-list-mode-map}
-Invoces `idris-hole-list-mode-hook'."
+(define-derived-mode idris-hole-list-mode special-mode "Idris Holes"
+  "Major mode used for transient Idris hole list buffers.
+\\{idris-hole-list-mode-map}
+Invokes `idris-hole-list-mode-hook'."
   (setq-local prop-menu-item-functions '(idris-context-menu-items)))
 
+;; TODO: Auto detect mode for idris holes buffer instead of
+;; invoking `idris-hole-list-mode' in `idris-hole-list-show'
+;; (push '("#\\*idris-holes\\*$" . idris-hole-list-mode) auto-mode-alist)
+
 (defun idris-hole-list-buffer ()
   "Return the Idris hole buffer, creating one if there is not one"
   (get-buffer-create idris-hole-list-buffer-name))
@@ -78,25 +81,23 @@ Invoces `idris-hole-list-mode-hook'."
       (progn (message "No holes found!")
              (idris-hole-list-quit))
     (with-current-buffer (idris-hole-list-buffer)
-      (setq buffer-read-only nil)
-      (erase-buffer)
       (idris-hole-list-mode)
-      (insert (propertize "Holes" 'face 'idris-info-title-face) "\n\n")
-      (when idris-show-help-text
-        (insert "This buffer displays the unsolved holes from the 
currently-loaded code. ")
-        (insert (concat "Press the "
-                        (if idris-enable-elab-prover "[E]" "[P]")
-                        " buttons to solve the holes interactively in the 
prover."))
-        (let ((fill-column 80))
-          (fill-region (point-min) (point-max)))
-        (insert "\n\n"))
-
-      (dolist (tree (mapcar #'idris-tree-for-hole hole-info))
-        (idris-tree-insert tree "")
-        (insert "\n\n"))
-      (message "Press q to close")
-      (setq buffer-read-only t)
-      (goto-char (point-min)))
+      (let ((buffer-read-only nil))
+        (erase-buffer)
+        (insert (propertize "Holes" 'face 'idris-info-title-face) "\n\n")
+        (when idris-show-help-text
+          (insert "This buffer displays the unsolved holes from the 
currently-loaded code. ")
+          (insert (concat "Press the "
+                          (if idris-enable-elab-prover "[E]" "[P]")
+                          " buttons to solve the holes interactively in the 
prover."))
+          (let ((fill-column 80))
+            (fill-region (point-min) (point-max)))
+          (insert "\n\n"))
+        (dolist (tree (mapcar #'idris-tree-for-hole hole-info))
+          (idris-tree-insert tree "")
+          (insert "\n\n"))
+        (message "Press q to close")
+        (goto-char (point-min))))
     (display-buffer (idris-hole-list-buffer))))
 
 (defun idris-hole-tree-printer (tree)
diff --git a/idris-tests.el b/idris-tests.el
index 367d4c2618..bd4113896a 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -73,7 +73,6 @@ remain."
 
 (ert-deftest idris-test-hole-load ()
   "Test the hole-list-on-load setting."
-  (idris-quit)
   ;;; The default setting should be to show holes
   (should idris-hole-show-on-load)
 



reply via email to

[Prev in Thread] Current Thread [Next in Thread]