| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
| 12.1 Default values for generic settings | ||
| 12.2 Adding prover-specific configurations | ||
| 12.3 Useful variables | ||
| 12.4 Useful functions and macros |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Several generic settings are defined using defpgcustom in
`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 defpgdefault macro:
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 myprover-home-page.
In the generic code, you can use a macro, writing (proof-ass
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.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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
and
<PA>-config for configuration of prover PA.
Typically <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
"http://findtheorem.myprover.org".
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
In `proof-site', several 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).
Non-nil if Proof General is running on GNU Emacs 21 or later.
Non-nil if Proof General is running on XEmacs.
Non-nil if Proof General is running on a win32 system.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The recommended functions you may invoke are these:
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.
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. |
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.
The function 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
buffer.
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-char 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.
There are several handy macros to help you define functions
which invoke proof-shell-invisible-command.
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.
Define command FN to send string body to proof assistant, based on cmdvar.
body defaults to cmdvar, a variable.
Define command FN to prompt for string cmdvar to proof assistant.
cmdvar is a variable holding a function or string. Automatically has history.
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 `expand-file-name').
%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.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.