feat: Add proof-upgrade-menu triggering proof-upgrade-elpa-packages

* require package.el (in a safe way thanks to `proof-try-require`)

2 files changed, 30 insertions, 8 deletions

diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index c8c2239b..3846229e 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -5,7 +5,7 @@
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
 ;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
-;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2010, 2016, 2021  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
 ;; Portions © Copyright 2015-2017  Clément Pit-Claudel
 
@@ -86,7 +86,6 @@ without adjusting window layout."
 	(pg-response-buffers-hint (buffer-name nextbuf))))))
 
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
 ;;; Key bindings
@@ -687,6 +686,10 @@ without adjusting window layout."
 	 (list (customize-menu-create 'proof-general-internals "Internals"))))
   "Advanced sub-menu of script functions and customize.")
 
+(defvar proof-upgrade-menu
+  '(["Upgrade ELPA packages..." proof-upgrade-elpa-packages
+     :help "Update all Emacs packages (including Proof General!)"])
+  "The Proof General generic menu for upgrading packages.")
 
 (defvar proof-menu
   '(["Next Error" proof-next-error
@@ -706,7 +709,8 @@ without adjusting window layout."
 	 proof-config-menu
 	 (list (customize-menu-create 'proof-user-options "Customize Options"))
 	 (list proof-advanced-menu)
-	 (list proof-help-menu))))
+	 (list proof-help-menu)
+         proof-upgrade-menu)))
 
 ;;;###autoload
 (defun proof-aux-menu ()
@@ -1053,10 +1057,6 @@ value) and the second for false."
 	(funcall proof-assistant-setting-format setting)
       setting)))
 
-
-
-
-
 (provide 'proof-menu)
 
 ;;; proof-menu.el ends here
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 39d1c22a..c5f4960d 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -5,7 +5,7 @@
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
 ;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
-;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2010, 2016, 2021  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
 ;; Portions © Copyright 2015-2017  Clément Pit-Claudel
 
@@ -101,6 +101,28 @@ Return nil if not a script buffer or if no active scripting buffer."
     (file-error nil))
   (featurep symbol))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Facility to upgrade all ELPA packages (including ProofGeneral)
+;;
+
+
+(defun proof-upgrade-elpa-packages ()
+  "Upgrade all ELPA packages (using package.el)."
+  (interactive)
+  (unless (proof-try-require 'package)
+    (error "The package feature is not available!"))
+  (let ((old-async package-menu-async))
+    (setq package-menu-async nil)
+    (package-list-packages)
+    (package-menu-mark-upgrades)
+    (let ((use-dialog-box nil))
+      ;; make `y-or-n-p' show up within the minibuffer
+      ;; even if `proof-upgrade-elpa-packages' is called interactively
+      ;; to avoid any dialog-box overflow if many packages are updated
+      (package-menu-execute))
+    (setq package-menu-async old-async)))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;