diff options
Diffstat (limited to 'generic/proof-toolbar.el')
-rw-r--r-- | generic/proof-toolbar.el | 320 |
1 files changed, 168 insertions, 152 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index c7d741dc..bccc6eb0 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -10,8 +10,28 @@ ;; proof-toolbar-menu which holds the same commands and is put on the ;; menubar by proof-toolbar-setup (surprisingly). ;; -;; Toolbar is just for scripting buffer at the moment. +;; Toolbar is just for the scripting buffer currently. ;; +;; +;; TODO: +;; +;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode) +;; Need a variable containing a specifier or similar. +;; (defvar proof-toolbar-specifier nil +;; "Specifier for proof toolbar.") +;; This doesn't seem worth fixing until XEmacs toolbar implementation +;; settles a bit. Enablers don't work too well at the moment. + +;; FIXME: it's a little bit tricky to add prover-specific items. +;; We can improve on that by generating everything on-thy-fly +;; in proof-toolbar-setup. + +;; FIXME: In the future, add back the enabler functions. +;; As of 20.4, they *almost* work, but it seems difficult +;; to get the toolbar to update at the right times. +;; For older versions of XEmacs (19.15, P.C.Callaghan@durham.ac.uk +;; reports) the toolbar specifier format doesn't like +;; arbitrary sexps as the enabler, either. ;;; IMPORT declaration @@ -19,49 +39,74 @@ (autoload 'proof-shell-live-buffer "proof-shell") (autoload 'proof-shell-restart "proof-shell") -(defconst proof-toolbar-default-button-list - '(proof-toolbar-goal-button - proof-toolbar-retract-button - proof-toolbar-undo-button - proof-toolbar-next-button - proof-toolbar-use-button - proof-toolbar-restart-button - proof-toolbar-qed-button - '[:style 3d] - nil) - "Example value for proof-toolbar-button-list. + +;; +;; The default generic toolbar +;; +(defconst proof-toolbar-entries-default + '((show "Show" "Show the current proof state" t) + (context "Context" "Show the current context" t) + (goal "Goal" "Start a new proof" t) + (retract "Retract" "Retract (undo) whole buffer" t) + (undo "Undo" "Undo the previous proof command" t) + (next "Next" "Process the next proof command" t) + (use "Use" "Process whole buffer" t) + (restart "Restart" "Restart scripting (clear all locked regions)" t) + (qed "QED" "Close/save proved theorem" t) + (command "Command" "Issue a non-scripting command") + (info "Info" "Show proof assistant information" t)) +"Example value for proof-toolbar-entries. This gives a bare toolbar that works for any prover. To add -prover specific buttons, see proof-toolbar.el.") +prover specific buttons, see documentation for proof-toolbar-entries +and the file proof-toolbar.el.") + +(defvar proof-toolbar-entries + proof-toolbar-entries-default + "List of entries for Proof General toolbar. +Format of each entry is (TOKEN MENUNAME TOOLBARTEXT ENABLER-P). +For each TOKEN, we expect an icon with base filename TOKEN, + a function proof-toolbar-<TOKEN>, + and (optionally) an enabler proof-toolbar-<TOKEN>-enable-p.") + + +;; +;; Function, icon, button names +;; + +(defun proof-toolbar-function (token) + (intern (concat "proof-toolbar-" (symbol-name token)))) + +(defun proof-toolbar-icon (token) + (intern (concat "proof-toolbar-" (symbol-name token) "-icon"))) + +(defun proof-toolbar-enabler (token) + (intern (concat "proof-toolbar-" (symbol-name token) "-enable-p"))) ;; ;; Menu built from toolbar functions ;; +(defun proof-toolbar-make-menu-item (tle) + "Make a menu item from a proof-toolbar-entries entry." + (let + ((token (car tle)) + (menuname (cadr tle)) + (tooltip (nth 2 tle)) + (enablep (nth 3 tle))) + (apply 'vector + (append + (list menuname (proof-toolbar-function token)) + (if enablep + (list ':active (list (proof-toolbar-enabler token)))))))) + (defconst proof-toolbar-menu - ;; Toolbar contains commands to manipulate script: "Scripting" - '("Scripting" - ["Goal" - proof-toolbar-goal - :active (proof-toolbar-goal-enable-p)] - ["Retract" - proof-toolbar-retract - :active (proof-toolbar-retract-enable-p)] - ["Undo" - proof-toolbar-undo - :active (proof-toolbar-undo-enable-p)] - ["Next" - proof-toolbar-next - :active (proof-toolbar-next-enable-p)] - ["Use" - proof-toolbar-use - :active (proof-toolbar-use-enable-p)] - ["Restart" - proof-toolbar-restart - :active (proof-toolbar-restart-enable-p)] - ["QED" - proof-toolbar-qed - :active (proof-toolbar-qed-enable-p)]) - "Menu made from the toolbar commands.") + ;; Toolbar contains commands to manipulate script and + ;; other handy stuff. Called "Scripting" + (append + '("Scripting") + (mapcar 'proof-toolbar-make-menu-item + proof-toolbar-entries)) + "Menu made from the Proof General toolbar commands.") ;; ;; Add this menu to proof-menu @@ -69,21 +114,54 @@ prover specific buttons, see proof-toolbar.el.") (setq proof-menu (append proof-menu (list proof-toolbar-menu))) +;; +;; Now the toolbar icons and buttons +;; + +(defun proof-toolbar-make-icon (tle) + "Make icon variable and icon list entry from a proof-toolbar-entries entry." + (let* ((icon (car tle)) + (iconname (symbol-name icon)) + (iconvar (proof-toolbar-icon icon))) + ;; first declare variable + ;; (eval + ;; `(defvar ,iconvar nil + ;; ,(concat + ;; "Glyph list for " iconname " button in Proof General toolbar."))) + ;; FIXME: above doesn't quite work right. However, we only lose + ;; the docstring which is no big deal. + ;; now the list entry + (list iconvar iconname))) + (defconst proof-toolbar-iconlist - '((proof-toolbar-next-icon "next") - (proof-toolbar-undo-icon "undo") - (proof-toolbar-retract-icon "retract") - (proof-toolbar-use-icon "use") - (proof-toolbar-goal-icon "goal") - (proof-toolbar-qed-icon "qed") - (proof-toolbar-restart-icon "restart")) + (mapcar 'proof-toolbar-make-icon proof-toolbar-entries) "List of icon variable names and their associated image files. A list of lists of the form (VAR IMAGE). IMAGE is the root name for an image file in proof-images-directory. The toolbar code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm and chooses the best one for the display properites.") -(defvar proof-toolbar-button-list proof-toolbar-default-button-list +(defun proof-toolbar-make-toolbar-item (tle) + "Make a toolbar button descriptor from a proof-toolbar-entries entry." + (let + ((token (car tle)) + (menuname (cadr tle)) + (tooltip (nth 2 tle)) + ;; FIXME: enabler now enabled, for testing at least. + ;; (enablep nil)) + (enablep (nth 3 tle))) + (vector + (proof-toolbar-icon token) + (proof-toolbar-function token) + (if enablep + (list (proof-toolbar-enabler token)) + t) + tooltip))) + +(defvar proof-toolbar-button-list + (append + (mapcar 'proof-toolbar-make-toolbar-item proof-toolbar-entries) + (list [:style 3d])) "A toolbar descriptor evaluated in proof-toolbar-setup. Specifically, a list of sexps which evaluate to entries in a toolbar descriptor. The default value proof-toolbar-default-button-list @@ -92,15 +170,6 @@ will work for any proof assistant.") (defvar proof-toolbar nil "Proof mode toolbar button list. Set in proof-toolbar-setup.") -;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode) -;; Need a variable containing a specifier or similar. -;; (defvar proof-toolbar-specifier nil -;; "Specifier for proof toolbar.") -;; This doesn't seem worth fixing until XEmacs toolbar implementation -;; settles a bit. Enablers don't work too well at the moment. - -;; FIXME: could automatically defvar the icon variables. - ;;; ###autoload (defun proof-toolbar-setup () "Initialize Proof General toolbar and enable it for the current buffer. @@ -140,117 +209,30 @@ to the default toolbar." (or force-on (not proof-toolbar-inhibit))) (proof-toolbar-setup)) + +;; +;; ================================================================= ;; -;; GENERIC PROOF TOOLBAR BUTTONS +;; +;; GENERIC PROOF TOOLBAR BUTTON FUNCTIONS ;; ;; Defaults functions are provided below for: up, down, restart ;; Code for specific provers may define the symbols below to use ;; the other buttons: next, prev, goal, qed (images are provided). ;; ;; proof-toolbar-next next function -;; proof-toolbar-next-enable enable predicate for next (or t) +;; proof-toolbar-next-enable enable predicate for next (or t) ;; ;; etc. ;; ;; To add support for more buttons or alter the default -;; images, proof-toolbar-iconlist should be adjusted. -;; +;; images, proof-toolbar-entries should be adjusted. ;; - -;; FIXME: In the future, add back the enabler functions. -;; As of 20.4, they *almost* work, but it seems difficult -;; to get the toolbar to update at the right times. -;; For older versions of XEmacs (19.15, P.C.Callaghan@durham.ac.uk -;; reports) the toolbar specifier format doesn't like -;; arbitrary sexps as the enabler, either. ;; -(defvar proof-toolbar-next-icon nil - "Glyph list for next button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-next-button - [proof-toolbar-next-icon - proof-toolbar-next - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-next-enable-p) - "Process the next proof command"]) - -(defvar proof-toolbar-undo-icon nil - "Glyph list for undo button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-undo-button - [proof-toolbar-undo-icon - proof-toolbar-undo - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-undo-enable-p) - "Undo the previous proof command"]) - -(defvar proof-toolbar-retract-icon nil - "Glyph list for retract button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-retract-button - [proof-toolbar-retract-icon - proof-toolbar-retract - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-retract-enable-p) - "Retract buffer"]) - -(defvar proof-toolbar-use-icon nil - "Glyph list for use button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-use-button - [proof-toolbar-use-icon - proof-toolbar-use - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-use-enable-p) - "Process whole buffer"]) - -(defvar proof-toolbar-restart-icon nil - "Glyph list for down button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-restart-button - [proof-toolbar-restart-icon - proof-toolbar-restart - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-restart-enable-p) - "Restart scripting"]) - -(defvar proof-toolbar-goal-icon nil - "Glyph list for goal button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-goal-button - [proof-toolbar-goal-icon - proof-toolbar-goal - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-goal-enable-p) - "Start a new proof"]) - -(defvar proof-toolbar-qed-icon nil - "Glyph list for QED button in proof toolbar. -Initialised in proof-toolbar-setup.") - -(defvar proof-toolbar-qed-button - [proof-toolbar-qed-icon - proof-toolbar-qed - ;; XEmacs isn't ready for enablers yet - t - ;; (proof-toolbar-qed-enable-p) - "Save proved theorem"]) - -;; -;; GENERIC PROOF TOOLBAR FUNCTIONS + +;; +;; Helper functions ;; (defmacro proof-toolbar-move (&rest body) @@ -267,7 +249,6 @@ Initialised in proof-toolbar-setup.") (proof-goto-end-of-queue-or-locked-if-not-visible))) - ;; ;; Undo button ;; @@ -391,8 +372,43 @@ Move point if the end of the locked position is invisible." (call-interactively 'proof-issue-save) (error "I can't see a completed proof!"))) +;; +;; Show button +;; + +(defun proof-toolbar-show-enable-p () + (proof-shell-available-p)) + +(defalias 'proof-toolbar-show 'proof-prf) +;; +;; Context button +;; +(defun proof-toolbar-context-enable-p () + (proof-shell-available-p)) + +(defalias 'proof-toolbar-context 'proof-ctxt) + +;; +;; Info button +;; +;; Might as well enable it all the time; convenient +;; way of starting proof assistant. +(defun proof-toolbar-info-enable-p () + t) + +(defalias 'proof-toolbar-info 'proof-help) + +;; +;; Command button +;; + +(defun proof-toolbar-command-enable-p () + (proof-shell-available-p)) + +(defalias 'proof-toolbar-command 'proof-execute-minibuffer-cmd) + ;; (provide 'proof-toolbar) |