diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 15 | ||||
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-script.el | 17 |
4 files changed, 44 insertions, 3 deletions
@@ -14,6 +14,10 @@ ** Generic Changes +*** Added proof assistant specific menu facility. + + Specific menus added for Coq, Isabelle. + *** Improved behaviour of electric terminator *** Efficiency improvement in parsing @@ -32,7 +36,9 @@ ** LEGO Changes -*** Slight change in output during proof: show final discharge messages +*** Slight change in output during proof: shows final discharge messages + + This is a side effect of code rationalization in PG elsewhere. ** Isabelle Changes diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 0083a54c..b2995081 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3534,6 +3534,19 @@ The following variables should be set in the script mode before @code{proof-config-done} is called. These make some settings for the commands and menus available in Proof General. +The first setting controls the proof-assistant specific menu, +if any is defined. + +@c TEXI DOCSTRING MAGIC: proof-assistant-menu-entries +@defvar proof-assistant-menu-entries +Entries for proof assistant specific menu. @* +A list of menu items [@var{name} @var{callback} ENABLE]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + +The remaining settings control the standard commands available +from the generic menu and the toolbar. + @c TEXI DOCSTRING MAGIC: proof-assistant-home-page @defvar proof-assistant-home-page Web address for information on proof assistant.@* @@ -3576,6 +3589,8 @@ If a function, it should return the command string to insert. + + @c defgroup proof-script @node Proof script settings @section Proof script settings 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 |