13. Writing More Lisp Code
You may want to add some extra features to your instance of Proof General which are not supported in the generic core. To do this, you can use the settings described above, plus a small number of fundamental functions in Proof General which you can consider as exported in the generic interface. Be careful using more functions than are mentioned here because the internals of Proof General may change between versions.
|13.1 Default values for generic settings|
|13.2 Adding prover-specific configurations|
|13.3 Useful variables|
|13.4 Useful functions and macros|
13.1 Default values for generic settings
Several generic settings are defined using
‘proof-config.el’. This introduces settings of the form
<PA>-name for each proof assistant PA.
To set the default value for these settings in prover-specific cases,
you should use the special
- Macro: defpgdefault
Set default for the proof assistant specific variable <PA>-sym to value.
This should be used in prover-specific code to alter the default values for prover specific settings.
Usage: (defpgdefault SYM value)
In your prover-specific code you can simply use the setting
<PA>-sym directly, i.e., write
In the generic code, you can use a macro, writing
home-page) to refer to the
<PA>-home-page setting for the
currently running instance of Proof General.
See section Configuration variable mechanisms, for more details on this mechanism.
13.2 Adding prover-specific configurations
Apart from the generic settings, your prover instance will probably need some specific customizable settings.
Defining new prover-specific settings using customize is pretty easy. You should do it at least for your prover-specific user options.
The code in ‘proof-site.el’ provides each prover with two
customization groups automatically (based on the name of the assistant):
<PA> for user options for prover PA
<PA>-config for configuration of prover PA.
<PA>-config holds settings which are
constants but which may be nice to tweak.
The first group appears in the menu
ProofGeneral -> Advanced -> Customize -> <PA>
The second group appears in the menu:
ProofGeneral -> Internals -> <PA> config
A typical use of
defcustom looks like this:
(defcustom myprover-search-page "http://findtheorem.myprover.org" "URL of search web page for myprover." :type 'string :group 'myprover-config)
This introduces a new customizable setting, which you might use to make
a menu entry, for example. The default value is the string
13.3 Useful variables
In ‘proof-site’, some architecture flags are defined. These can be used to write conditional pieces of code for different Emacs and operating systems. They are referred to mainly in ‘proof-compat’ (which helps to keep the architecture and version dependent code in one place).
13.4 Useful functions and macros
The recommended functions you may invoke are these:
- Any of the interactive commands (i.e. anything you can invoke with M-x, including all key-bindings)
- Any of the internal functions and macros mentioned below
To insert text into the current (usually script) buffer, the function
proof-insert is useful. There’s also a handy macro
proof-defshortcut for defining shortcut functions using it.
- Function: proof-insert text
Insert text into the current buffer.
text may include these special characters:
%p - place the point here after input
Any other %-prefixed character inserts itself.
- Macro: proof-defshortcut
Define shortcut function FN to insert string, optional keydef KEY.
This is intended for defining proof assistant specific functions. string is inserted using ‘
proof-insert’, which see. KEY is added onto proof assistant map.
proof-shell-invisible-command is a useful utility
for sending a single command to the process. You should use this to
implement user-level or internal functions rather than attempting to
directly manipulate the proof action list, or insert into the shell
- Function: proof-shell-invisible-command cmd &optional wait invisiblecallback &rest flags
Send cmd to the proof process.
The cmd is ‘invisible’ in the sense that it is not recorded in buffer. cmd may be a string or a string-yielding expression.
Automatically add ‘
proof-terminal-string’ if necessary, examining ‘proof-shell-no-auto-terminate-commands’.
By default, let the command be processed asynchronously. But if optional wait command is non-nil, wait for processing to finish before and after sending the command.
In case cmd is (or yields) nil, do nothing.
invisiblecallback will be invoked after the command has finished, if it is set. It should probably run the hook variables ‘
flags are additional flags to put onto the ‘
proof-action-list’. The flag
'invisibleis always added to flags.
There are several handy macros to help you define functions
- Macro: proof-definvisible
Define function FN to send string to proof assistant, optional keydef KEY.
This is intended for defining proof assistant specific functions. string is sent using ‘
proof-shell-invisible-command’, which see. string may be a string or a function which returns a string. KEY is added onto proof assistant map.
- Macro: proof-define-assistant-command
Define FN (docstring DOC): check if cmdvar is set, then send body to prover.
body defaults to cmdvar, a variable.
- Macro: proof-define-assistant-command-witharg
Define FN (arg) with DOC: check cmdvar is set, prompt a string and eval body.
The body can contain occurrences of arg. cmdvar is a variable holding a function or string. Automatically has history.
- Function: proof-format-filename string filename
Format string by replacing quoted chars by escaped version of filename.
%e uses the canonicalized expanded version of filename (including directory, using ‘
default-directory’ – see ‘
%r uses the unadjusted (possibly relative) version of filename.
%m (’module’) uses the basename of the file, without directory or extension.
%s means the same as %e.
Using %e can avoid problems with dumb proof assistants who don’t understand ~, for example.
For all these cases, the escapes in ‘
proof-shell-filename-escapes’ are processed.
If string is in fact a function, instead invoke it on filename and return the resulting (string) value.
This document was generated by Erik Martin-Dorel on March 10, 2022 using texi2html 1.82.