diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 95 | ||||
| -rw-r--r-- | generic/proof-menu.el | 12 | ||||
| -rw-r--r-- | generic/proof-script.el | 34 | ||||
| -rw-r--r-- | generic/proof-useropts.el | 14 |
4 files changed, 132 insertions, 23 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index fca238f8..f8b2c265 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -86,7 +86,7 @@ Assumes that point is at the end of a command." "Move point according to `proof-follow-mode'. If optional POS is set, use that position, else `proof-queue-or-locked-end'. Assumes script buffer is current." - (unless (eq proof-follow-mode 'ignore) + (unless (or proof-autosend-running (eq proof-follow-mode 'ignore)) (let ((dest (or pos (proof-queue-or-locked-end)))) (cond ((eq proof-follow-mode 'locked) @@ -940,7 +940,8 @@ If NUM is negative, move upwards. Return new span." ((proof-locked-region-full-p) (pg-hint (concat "Processing complete in " (buffer-name proof-script-buffer)))) - (t ;; partly complete: hint about displaying the locked end + ((not proof-autosend-running) + ;; partly complete: hint about displaying the locked end (pg-jump-to-end-hint)))))))) ;;;###autoload @@ -1405,6 +1406,96 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." (car undo-list))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Automatic processing of buffer ahead of point +;; +;; Added in PG 4.0 +;; + +(defvar proof-autosend-timer nil "Timer used by autosend.") + +;;;###autoload +(defun proof-autosend-enable (&optional nomsg) + "Enable or disable autosend behaviour." + (if proof-autosend-timer + (cancel-timer proof-autosend-timer)) + (when proof-autosend-enable + (setq proof-autosend-timer + (run-with-idle-timer proof-autosend-delay + t 'proof-autosend-loop)) + (unless nomsg (message "Automatic sending turned on."))) + (when (not proof-autosend-enable) + (setq proof-autosend-timer nil) + (unless nomsg (message "Automatic sending turned off.")))) + +(defun proof-autosend-delay () + "Adjust autosend timer when variable `proof-autosend-delay' changes." + (proof-autosend-enable t)) + +(defvar proof-autosend-running nil + "Flag indicating we are sending commands to the prover automatically.") + +(defun proof-autosend-loop () + (proof-with-current-buffer-if-exists proof-script-buffer + (unless (proof-locked-region-full-p) + (proof-autosend-loop1)))) + +(defun proof-autosend-loop1 () + "Send commands from the script until an error, complete, or input appears." + (let ((making-progress t) last-locked-end) + (setq proof-autosend-running t) + (message "Sending commands to prover...") + (unwind-protect + (progn + (save-excursion + ;; TODO: try it in chunks + (goto-char (point-max)) + (proof-assert-until-point + (if proof-multiple-frames-enable + 'no-minibuffer-messages ; nb: not API but n + '(no-response-display + no-error-display + no-goals-display)))) + (proof-shell-wait t) ; interruptible + (if (input-pending-p) + ;; stop things here + (proof-interrupt-process))) + (setq proof-autosend-running nil)) + (message "Sending commands to prover...done."))) + + +;; alternative incremental, less aggressive version of above +(defun proof-autosend-loop1-old () + "Send commands from the script until an error, complete, or input appears." + (let ((making-progress t) last-locked-end) + (setq proof-autosend-running t) + (message "Sending commands to prover...") + (unwind-protect + (while (and making-progress (not (input-pending-p))) + (setq last-locked-end (proof-unprocessed-begin)) + (save-excursion + (goto-char last-locked-end) + (skip-chars-forward " \t\n") + (proof-assert-until-point + (if proof-multiple-frames-enable nil + '(no-response-display + no-error-display + no-goals-display + no-point-movement)))) + (proof-shell-wait) + (setq making-progress (> (proof-unprocessed-begin) + last-locked-end))) + ;; FIXME: not quite right behaviour: proof-done-advancing can + ;; still move point afterwards when prover output is processed, + ;; even though we didn't want that to happen. + ;; Really we should obey no-point-movement above. + (setq proof-autosend-running nil)) + (message "Sending commands to prover...done."))) + + + (provide 'pg-user) ;;; pg-user.el ends here diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 7ab7a3ae..4c98435e 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -135,6 +135,7 @@ without adjusting window layout." (define-key map [(control meta down)] 'pg-move-region-down) ;; (define-key map [(control c) ?b] 'proof-toolbar-toggle) + (define-key map [(control c) ?>] 'proof-autosend-toggle) ;; Add the universal keys bound in all PG buffers. ;; NB: C-c ` is next-error in universal-keys (proof-define-keys map proof-universal-keys)) @@ -291,12 +292,12 @@ without adjusting window layout." (proof-deftoggle proof-sticky-errors) (proof-deftoggle proof-shell-quiet-errors) (proof-deftoggle proof-minibuffer-messages) -(proof-deftoggle proof-autosend) - -(proof-deftoggle-fn 'proof-imenu-enable 'proof-imenu-toggle) +(proof-deftoggle proof-autosend-enable proof-autosend-toggle) +(proof-deftoggle proof-imenu-enable proof-imenu-toggle) (proof-deftoggle proof-keep-response-history) (proof-eval-when-ready-for-assistant + ;; togglers for settings separately configurable per-prover (proof-deftoggle-fn (proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle) (proof-deftoggle-fn @@ -318,6 +319,10 @@ without adjusting window layout." :style toggle :selected proof-electric-terminator-enable :help "Automatically send commands as typed"] + ["Send Automatically" proof-autosend-toggle + :style toggle + :selected proof-autosend-enable + :help "Automatically send commands when idle"] ["Fly Past Comments" proof-script-fly-past-comments-toggle :style toggle :selected proof-script-fly-past-comments @@ -505,6 +510,7 @@ without adjusting window layout." "Return a list of the quick option variables." (list 'proof-electric-terminator-enable + 'proof-autosend-enable 'proof-script-fly-past-comments 'proof-disappearing-proofs 'proof-full-annotation diff --git a/generic/proof-script.el b/generic/proof-script.el index 7e3055b4..be2b84ca 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -319,10 +319,11 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (infop (span-live-p badspan))) (proof-detach-queue) (when infop - (when (eq proof-follow-mode 'locked) - ;; jump to start of error: should this be configurable? - (goto-char (span-start badspan)) - (skip-chars-forward " \t\n")) + (unless proof-autosend-running + (when (eq proof-follow-mode 'locked) + ;; jump to start of error: should this be configurable? + (goto-char (span-start badspan)) + (skip-chars-forward " \t\n"))) (when proof-sticky-errors (pg-set-span-helphighlights badspan 'proof-script-highlight-error-face @@ -442,6 +443,7 @@ Does nothing if there is no active scripting buffer, or if `proof-follow-mode' is set to 'ignore." (interactive) (if (and proof-script-buffer + (not proof-autosend-running) (not (eq proof-follow-mode 'ignore))) (unless (proof-end-of-locked-visible-p) (proof-goto-end-of-locked t)))) @@ -450,15 +452,14 @@ Does nothing if there is no active scripting buffer, or if "As `proof-goto-end-of-locked-if-pos-not-visible-in-window', but not for interrupts. Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (interactive) - (cond - ((eq proof-follow-mode 'ignore)) - ((eq proof-shell-last-output-kind 'error) - (proof-goto-end-of-locked-if-pos-not-visible-in-window))) - (proof-with-current-buffer-if-exists - proof-script-buffer - ;; Give a hint of how to jump to the end of locked, unless visible. - (unless (proof-end-of-locked-visible-p) - (pg-jump-to-end-hint)))) + (unless proof-autosend-running + (unless (eq proof-follow-mode 'ignore) + (if (eq proof-shell-last-output-kind 'error) + (proof-goto-end-of-locked-if-pos-not-visible-in-window))) + (proof-with-current-buffer-if-exists + proof-script-buffer + (unless (proof-end-of-locked-visible-p) + (pg-jump-to-end-hint))))) (defun proof-end-of-locked-visible-p () "Return non-nil if end of locked region is visible." @@ -1118,7 +1119,7 @@ a scripting buffer is killed it is always retracted." ;; Make status of inactive scripting buffer show up (necessary?) (force-mode-line-update) - ;; Finally, run hooks (added in 3.5 22.04.04) + ;; Finally, run hooks (run-hooks 'proof-deactivate-scripting-hook)))))) (defun proof-activate-scripting (&optional nosaves queuemode) @@ -1172,7 +1173,7 @@ activation is considered to have failed and an error is given." ;; If automatic retraction happened in the above step, we may ;; have inadvertently activated scripting somewhere else. - ;; Better turn it off again. This should succeed trivially. + ;; Better turn it off again. This should succeed trivially. ;; NB: it seems that we could move the first test for an already ;; active buffer here, but it is more subtle: the first ;; deactivation can extend the proof-included-files list, which @@ -2515,6 +2516,9 @@ finish setup which depends on specific proof assistant configuration." (or (buffer-file-name) (setq buffer-offer-save t)) + ;; Turn on autosend if enabled + (proof-autosend-enable 'nomsg) + ;; Finally, make sure the user has been welcomed! ;; [NB: this doesn't work well, can get zapped by loading messages] (proof-splash-message)) diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 7286f9a6..5bd050dd 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -281,9 +281,6 @@ This variable exists to disable the cache in case of problems." :type 'boolean :group 'proof-user-options) - -;;; NON BOOLEAN OPTIONS - (defcustom proof-follow-mode 'locked "*Choice of how point moves with script processing commands. One of the symbols: 'locked, 'follow, 'followdown, 'ignore. @@ -377,6 +374,17 @@ are distracting or too frequent." :type 'boolean :group 'proof-user-options) +(defcustom proof-autosend-enable nil + "*Non-nil causes Proof General to automatically process the script." + :type 'boolean + :set 'proof-set-value + :group 'proof-user-options) + +(defcustom proof-autosend-delay 0.8 + "*Delay before autosend starts sending commands." + :type 'float + :set 'proof-set-value + :group 'proof-user-options) |