2. Menus, toolbar, and user-level commands

The variables described in this chapter configure the menus, toolbar, and user-level commands. They should be set in the script mode before proof-config-done is called. (Toolbar configuration must be made before ‘proof-toolbar.el’ is loaded, which usually is triggered automatically by an attempt to display the toolbar).

2.1 Settings for generic user-level commands

Variable: proof-assistant-home-page

Web address for information on proof assistant.
Used for Proof General’s help menu.

Variable: proof-context-command

Command to display the context in proof assistant.

Variable: proof-info-command

Command to ask for help or information in the proof assistant.
String or fn. If a string, the command to use. If a function, it should return the command string to insert.

Variable: proof-showproof-command

Command to display proof state in proof assistant.

Variable: proof-goal-command

Command to set a goal in the proof assistant. String or fn.
If a string, the format character ‘%s’ will be replaced by the goal string. If a function, it should return the command string to insert.

Variable: proof-save-command

Command to save a proved theorem in the proof assistant. String or fn.
If a string, the format character ‘%s’ will be replaced by the theorem name. If a function, it should return the command string to insert.

Variable: proof-find-theorems-command

Command to search for a theorem containing a given term. String or fn.
If a string, the format character ‘%s’ will be replaced by the term. If a function, it should return the command string to send.

2.2 Menu configuration

As well as the generic Proof General menu, each proof assistant is provided with a specific menu which can have prover-specific commands. Proof General puts some default things on this menu, including the commands to start/stop the prover, and the user-extensible "Favourites" menu.

Variable: PA-menu-entries

Extra entries for proof assistant specific menu.
A list of menu items [name callback enabler ...]. See the documentation of ‘easy-menu-define’ for more details.

Variable: PA-help-menu-entries

Extra entries for help submenu for proof assistant specific help menu.
A list of menu items [name callback enabler ...]. See the documentation of ‘easy-menu-define’ for more details.

2.3 Toolbar configuration

Unlike the menus, Proof General has only one toolbar. For the "generic" aspect of Proof General to work well, we shouldn’t change (the meaning of) the existing toolbar buttons too far. This would discourage people from experimenting with different proof assistants when they don’t really know them, which is one of the advantages that Proof General brings.

But in case it is hard to map some of the generic buttons onto functions in particular provers, and to allow extra buttons, there is a mechanism for adjustment.

I used The Gimp to create the buttons for Proof General. The development distribution includes a button blank and some notes in ‘etc/notes.txt’ about making new buttons.

Variable: proof-toolbar-entries-default

Example value for proof-toolbar-entries. Also used to define scripting menu.
This gives a bare toolbar that works for any prover, providing the appropriate configuration variables are set. To add/remove prover specific buttons, adjust the ‘<PA>-toolbar-entries’ variable, and follow the pattern in ‘proof-toolbar.el’ for defining functions, images.

Variable: PA-toolbar-entries

List of entries for Proof General toolbar and Scripting menu.
Format of each entry is (token menuname tooltip toolbar-p [VISIBLE-P]).

For each token, we expect an icon with base filename token, a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler proof-toolbar-<TOKEN>-enable-p.

If visible-p is absent, or evaluates to non-nil, the item will appear on the toolbar or menu. If it evaluates to nil, the item is not shown.

If menuname is nil, item will not appear on the scripting menu.

If toolbar-p is nil, item will not appear on the toolbar.

The default value is ‘proof-toolbar-entries-default’ which contains the standard Proof General buttons.

Here’s an example of how to remove a button, from ‘af2.el’:

(setq af2-toolbar-entries
      (assq-delete-all 'state af2-toolbar-entries))

This document was generated on November 21, 2024 using texi2html 1.82.