diff options
| -rw-r--r-- | generic/proof-script.el | 30 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 117 |
2 files changed, 110 insertions, 37 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index b7334087..38c66487 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -180,6 +180,21 @@ buffer to END." (span-end proof-locked-span)) (point-min))) +;; da: NEW function added 28.10.98. This seems more +;; appropriate point to move point to (or make sure is displayed) +;; when a queue of commands is being processed. The locked +;; end may be further away. +(defun proof-queue-or-locked-end () + "Return the end of the queue region, or locked region, or (point-min). +This position should be the first writable position in the buffer." + (if (member (current-buffer) proof-script-buffer-list) + (cond (proof-queue-span + (span-end proof-queue-span)) + (proof-locked-span + (span-end proof-locked-span)) + (t + (point-min))))) + (defun proof-locked-end () "Return end of the locked region of the current buffer. Only call this from a scripting buffer." @@ -458,7 +473,8 @@ the hooks `proof-activate-scripting-hook' are run." (< (point) (proof-locked-end))) (defun proof-goto-end-of-locked-if-pos-not-visible-in-window () - "If the end of the locked region is not visible, jump to the end of it." + "If the end of the locked region is not visible, jump to the end of it. +A possible hook function for proof-shell-handle-error-hook." (interactive) (let* ((proof-script-buffer (car proof-script-buffer-list)) (pos (save-excursion @@ -468,6 +484,18 @@ the hooks `proof-activate-scripting-hook' are run." proof-script-buffer t)) (proof-goto-end-of-locked-interactive)))) +;; da: NEW function added 28.10.98. +;; This is used by toolbar follow mode (which used to use the function +;; above). [But wouldn't work for proof-shell-handle-error-hook?]. + +(defun proof-goto-end-of-queue-or-locked-if-not-visible () + "Jump to the end of the queue region or locked region if it isn't visible. +Assumes script buffer is current" + (unless (pos-visible-in-window-p + (proof-queue-or-locked-end) + (get-buffer-window (current-buffer) t)) + (goto-char (proof-queue-or-locked-end)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 68c73834..84a09dad 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -11,16 +11,6 @@ ;; (require 'proof-script) -(require 'proof-shell) - -;; FIXME: would be nice to have proof-shell autoloaded when shell is -;; actually started. Need to fixup references to variables here to be -;; autoloaded functions from proof-shell, and remove from enablers. - -(defcustom proof-toolbar-wanted t - "*Whether to use toolbar in proof mode." - :type 'boolean - :group 'proof) (defconst proof-toolbar-default-button-list '(proof-toolbar-goal-button @@ -216,58 +206,105 @@ Initialised in proof-toolbar-setup.") ;; GENERIC PROOF TOOLBAR FUNCTIONS ;; +(defmacro proof-toolbar-move (&rest body) + "Save point according to proof-toolbar-follow-mode, execute BODY." + `(if (eq proof-toolbar-follow-mode 'locked) + (progn + ,@body) ; nb no error catching + (save-excursion + ,@body))) + +(defun proof-toolbar-follow () + "Maybe point to the make sure the locked region is displayed." + (if (eq proof-toolbar-follow-mode 'follow) + (proof-goto-end-of-queue-or-locked-if-not-visible))) + + + +;; +;; Undo button +;; + (defun proof-toolbar-undo-enable-p () (and (proof-shell-available-p) (> (proof-unprocessed-begin) (point-min)))) +;; No error if enabler fails: if it is because proof shell is busy, +;; it gets messy when clicked quickly in succession. + (defun proof-toolbar-undo () "Undo last successful in locked region, without deleting it." (interactive) (if (proof-toolbar-undo-enable-p) - (save-excursion - (proof-undo-last-successful-command t)) - (error "I don't know what I should undo in this buffer!"))) + (progn + (proof-toolbar-move + (proof-undo-last-successful-command t)) + (proof-toolbar-follow)))) + +;; +;; Next button +;; (defun proof-toolbar-next-enable-p () - ;; Could check if there *is* a next command here, to avoid - ;; stupid "nothing to do" errors. - t) + (and + (not (proof-locked-region-full-p)) + (not (and (proof-shell-live-buffer) proof-shell-busy)))) + +;; No error if enabler fails: if it is because proof shell is busy, +;; it gets messy when clicked quickly in succession. (defun proof-toolbar-next () "Assert next command in proof to proof process. Move point if the end of the locked position is invisible." (interactive) - (save-excursion - (if (proof-shell-live-buffer) - (goto-char (proof-unprocessed-begin)) - (goto-char (point-min))) - (proof-assert-next-command)) - ;; FIXME: not sure about whether this is nice or not. - (proof-goto-end-of-locked-if-pos-not-visible-in-window)) + (if (proof-toolbar-next-enable-p) + (progn + (proof-toolbar-move + (goto-char (proof-unprocessed-begin)) + (proof-assert-next-command)) + (proof-toolbar-follow)))) + + +;; +;; Retract button +;; (defun proof-toolbar-retract-enable-p () - (and (proof-shell-available-p) - (member (current-buffer) proof-script-buffer-list))) + (and (member (current-buffer) proof-script-buffer-list) + (not (proof-locked-region-empty-p)))) (defun proof-toolbar-retract () - "Retract buffer." + "Retract entire buffer." ;; proof-retract-file might be better here! (interactive) (if (proof-toolbar-retract-enable-p) - (save-excursion - (goto-char (point-min)) - (proof-retract-until-point)))) + (progn + (proof-toolbar-move + (goto-char (point-min)) + (proof-retract-until-point)) ; gives error if process busy + (proof-toolbar-follow)) + (error "Nothing to retract in this buffer!"))) + +;; +;; Use button +;; (defun proof-toolbar-use-enable-p () - ;; Could check to see that whole buffer hasn't been - ;; processed already. - t) + (not (proof-locked-region-full-p))) (defun proof-toolbar-use () "Process the whole buffer" (interactive) - (save-excursion - (proof-process-buffer))) + (if (proof-toolbar-use-enable-p) + (progn + (proof-toolbar-move + (proof-process-buffer)) ; gives error if process busy + (proof-toolbar-follow)) + (error "There's nothing to do in this buffer!"))) + +;; +;; Restart button +;; (defun proof-toolbar-restart-enable-p () ;; Could disable this unless there's something running. @@ -280,13 +317,21 @@ Move point if the end of the locked position is invisible." (if (yes-or-no-p (concat "Restart " proof-assistant " scripting?")) (proof-restart-script)))) +;; +;; Goal button +;; + (defun proof-toolbar-goal-enable-p () ;; Goals are always allowed: will crank up process if need be. + ;; Actually this should only be available when "no subgoals" t) (defalias 'proof-toolbar-goal 'proof-issue-goal) -;; Actually this should only be available when "no subgoals" + +;; +;; QED button +;; (defun proof-toolbar-qed-enable-p () (and proof-shell-proof-completed @@ -299,4 +344,4 @@ Move point if the end of the locked position is invisible." (call-interactively 'proof-issue-save) (error "I can't see a completed proof!"))) ;; -(provide 'proof-toolbar)
\ No newline at end of file + (provide 'proof-toolbar) |