[nongnu] elpa/idris-mode 9e931bf1ff 07/12: Mark `idris-list-holes-on-load` as obsolete in favour of `idris-list-holes`

[ELPA Syncer]

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

    Mark `idris-list-holes-on-load` as obsolete in favour of `idris-list-holes`
    
    Why:
    The `idris-list-holes-on-load` was defined as interactive and such
    as invokable by user but with nondeterministic behaviour affected
    by `idris-hole-show-on-load`.
    Removing it in future will simplify the public api of idris-mode
    and reduce maintainance costs.
    
    This commit also updates docs for `idris-prover-success-hook`
    and `idris-load-file-success-hook` to make explicit that
    they are also affected by the `idris-hole-show-on-load` variable.
---
 idris-commands.el | 14 ++------------
 idris-prover.el   |  6 ------
 idris-settings.el | 28 +++++++++++++++++++++++-----
 inferior-idris.el |  9 +++++++++
 4 files changed, 34 insertions(+), 23 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index c1c8f3bfcd..6c7b24dcee 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -109,18 +109,8 @@
             (setq idris-process-current-working-directory 
new-working-directory))
         (error "Failed to switch the working directory %s" eval-result)))))
 
-(defun idris-list-holes-on-load ()
-  "Use the user's settings from customize to determine whether to list the 
holes."
-  (interactive)
-  (when idris-hole-show-on-load (idris-list-holes)))
-
-(defcustom idris-load-file-success-hook '(idris-list-holes-on-load
-                                          idris-set-current-pretty-print-width)
-  "Functions to call when loading a file is successful"
-  :type 'hook
-  :options '(idris-list-holes-on-load
-             idris-set-current-pretty-print-width)
-  :group 'idris)
+(define-obsolete-function-alias 'idris-list-holes-on-load 'idris-list-holes 
"2022-12-15"
+   "Use the user's settings from customize to determine whether to list the 
holes.")
 
 (defun idris-possibly-make-dirty (beginning end _length)
   ;; If there is a load-to-here marker and a currently loaded region, only
diff --git a/idris-prover.el b/idris-prover.el
index 9e00755e4e..9a4ea45c2b 100644
--- a/idris-prover.el
+++ b/idris-prover.el
@@ -436,12 +436,6 @@ the length reported by Idris."
      t)
     (_ nil)))
 
-(defcustom idris-prover-success-hook '(idris-list-holes-on-load)
-  "Functions to call when completing a proof"
-  :type 'hook
-  :options '(idris-list-holes-on-load)
-  :group 'idris-prover)
-
 (defun idris-perhaps-insert-proof-script (proof)
   "Prompt the user as to whether PROOF should be inserted into the buffer."
   (save-window-excursion
diff --git a/idris-settings.el b/idris-settings.el
index 4eabb7c5ac..16d3365a5a 100644
--- a/idris-settings.el
+++ b/idris-settings.el
@@ -230,8 +230,8 @@ customize the display of non-code text."
   :group 'idris)
 
 (defcustom idris-hole-list-show-expanded t
-  "Show the hole list fully expanded by default. This may be useful
-on wide monitors with lots of space for the hole buffer."
+  "Show the hole list fully expanded by default.
+This may be useful on wide monitors with lots of space for the hole buffer."
   :type 'boolean
   :group 'idris-hole-list)
 
@@ -251,6 +251,24 @@ change to ordinary prover interaction."
   :group 'idris
   :options '(idris-set-current-pretty-print-width))
 
+(defcustom idris-load-file-success-hook '(idris-list-holes
+                                          idris-set-current-pretty-print-width)
+  "Functions to call when loading a file is successful.
+When `idris-hole-show-on-load' is set to nil the function `idris-list-holes'
+will be removed from the list automatically and will not be executed."
+  :type 'hook
+  :options '(idris-list-holes
+             idris-set-current-pretty-print-width)
+  :group 'idris)
+
+(defcustom idris-prover-success-hook '(idris-list-holes)
+  "Functions to call when completing a proof.
+When `idris-hole-show-on-load' is set to nil the function `idris-list-holes'
+will be removed from the list automatically and will not be executed."
+  :type 'hook
+  :options '(idris-list-holes)
+  :group 'idris-prover)
+
 ;;;; REPL settings
 
 (defgroup idris-repl nil "Idris REPL" :prefix 'idris :group 'idris)
@@ -299,10 +317,10 @@ Set to `nil' for no banner."
   "File to save the persistent REPL history to.
 
 By default we assume Idris' default configuration home is:
- 
+
   $HOME/.idris/idris-history.eld.
-     
-If you have installed/configured Idris differently, or are 
+
+If you have installed/configured Idris differently, or are
 using Idris2, then you may wish to customise this variable."
 
   :type 'string
diff --git a/inferior-idris.el b/inferior-idris.el
index 8c2ae7b89c..571166dcf7 100644
--- a/inferior-idris.el
+++ b/inferior-idris.el
@@ -142,6 +142,15 @@ directory variables.")
     (add-hook 'idris-event-hooks 'idris-log-hook-function)
     (add-hook 'idris-event-hooks 'idris-warning-event-hook-function)
     (add-hook 'idris-event-hooks 'idris-prover-event-hook-function)
+
+    (unless idris-hole-show-on-load
+      (remove-hook 'idris-load-file-success-hook 'idris-list-holes-on-load)
+      (remove-hook 'idris-load-file-success-hook 'idris-list-holes)
+      ;; TODO: In future decouple prover sucess hook from being affected by
+      ;; idris-hole-show-on-load variable
+      (remove-hook 'idris-prover-success-hook 'idris-list-holes-on-load)
+      (remove-hook 'idris-prover-success-hook 'idris-list-holes))
+
     (set-process-filter idris-connection 'idris-output-filter)
     (set-process-sentinel idris-connection 'idris-sentinel)
     (set-process-query-on-exit-flag idris-connection t)