aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el8
-rw-r--r--generic/proof-shell.el9
2 files changed, 14 insertions, 3 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index cf090aa1..cb24657f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1552,9 +1552,11 @@ if you don't need it (slight speed penalty)."
(defcustom proof-shell-extend-queue-hook nil
"Hooks run by proof-extend-queue before extending `proof-action-list'.
-Can be used to run additional actions before items are added to the queue
-\(such as recompiling required modules for Coq) or to modify the items
-that are going to be added to `proof-action-list'."
+Can be used to run additional actions before items are added to
+the queue \(such as compiling required modules for Coq) or to
+modify the items that are going to be added to
+`proof-action-list'. The items that are about to be added are
+bound to `queueitems'."
:type '(repeat function)
:group 'proof-shell)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f5825516..dcd36a6c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -922,6 +922,15 @@ This function calls `proof-add-to-queue'."
(proof-set-queue-endpoints start end))
(proof-add-to-queue queueitems queuemode))
+
+(defvar queueitems
+ "Local variable of `proof-extend-queue' and `proof-shell-extend-queue-hook'.
+This only locally used variable communicates the items that are
+about to be placed into the `proof-action-list' queue into the
+hook functions in `proof-shell-extend-queue-hook'. This is the
+price to pay for using a normal hook.")
+
+
;;;###autoload
(defun proof-extend-queue (end queueitems)
"Extend the current queue with QUEUEITEMS, queue end END.