diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-01 18:18:30 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-01 18:18:30 +0000 |
| commit | e9ac9e8eb3d2567ff1ab12cf7bfdd60d5df2c30f (patch) | |
| tree | 2174f36ab1eb25c86534c6b95177634c11a6f2c2 /generic | |
| parent | e3b0ad751924c57db4ec8e72759edd2070757097 (diff) | |
Added proof-assistant-menu-entries for proof assistant specific menus.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-script.el | 17 |
2 files changed, 22 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 874a53fc..dc39cc62 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -682,6 +682,13 @@ If a function, it should return the command string to insert." :type '(choice string function) :group 'prover-config) +(defcustom proof-assistant-menu-entries nil + "Entries for proof assistant specific menu. +A list of menu items [NAME CALLBACK ENABLE]. See the documentation +of `easy-menu-define' for more details." + :type 'sexp + :group 'prover-config) + diff --git a/generic/proof-script.el b/generic/proof-script.el index 6d2708b2..933bf1df 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2346,8 +2346,11 @@ This is intended as a value for proof-activate-scripting-hook" :active (fboundp 'function-menu)] "----") proof-shared-menu) - "The menu for the proof assistant.") + "The Proof General generic menu.") +(defvar proof-assistant-menu + nil + "The Proof General proof-assistant specific menu.") @@ -2723,7 +2726,7 @@ finish setup which depends on specific proof assistant configuration." ;; NB: autloads proof-toolbar, which defines proof-toolbar-scripting-menu. (proof-toolbar-setup) - ;; Menu + ;; Menus (easy-menu-define proof-mode-menu proof-mode-map "Proof General menu" @@ -2748,6 +2751,16 @@ finish setup which depends on specific proof assistant configuration." ;; Put the ProofGeneral menu on the menubar (easy-menu-add proof-mode-menu proof-mode-map) + ;; Deal with the proof assistant specific menu + (if proof-assistant-menu-entries + (progn + (easy-menu-define proof-assistant-menu + proof-mode-map + proof-assistant + (cons proof-assistant + proof-assistant-menu-entries)) + (easy-menu-add proof-assistant-menu proof-mode-map))) + ;; Make sure func menu is configured. (NB: Ideal place for this and ;; similar stuff would be in something evaluated at top level after |