| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter sketches some of the internal functions and variables of Proof General, to help developers who wish to understand or modify the code.
Most of the documentation below is generated automatically from the comments in the code. Because Emacs lisp is interpreted and self-documenting, the best way to find your way around the source is inside Emacs once Proof General is loaded. Read the source files, and use functions such as C-h v and C-h f.
The code is split into files. The following sections document the important files, kept in the `generic/' subdirectory.
| 13.1 Spans | ||
| 13.3 Configuration variable mechanisms | ||
| 13.2 Proof General site configuration | ||
| 13.4 Global variables | ||
| 13.5 Proof script mode | ||
| 13.6 Proof shell mode | ||
| 13.7 Debugging |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Spans are an abstraction of XEmacs extents used to help bridge the gulf between GNU Emacs and XEmacs. In GNU Emacs, spans are implemented using overlays.
See the files `span-extent.el' and `span-overlay.el' for the implementation of the common interface in each case.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The file `proof-site.el' contains the initial configuration for Proof General for the site (or user) and the choice of provers.
The first part of the configuration is to set
proof-home-directory to the directory that `proof-site.el'
is located in, or to the variable of the environment variable
PROOFGENERAL_HOME if that is set.
Directory where Proof General is installed. Ends with slash.
Default value taken from environment variable `PROOFGENERAL_HOME' if set,
otherwise based on where the file `proof-site.el' was loaded from.
You can use customize to set this variable.
Further directory variables allow the files of Proof General to be split
up and installed across a system if need be, rather than under the
proof-home-directory root.
Where Proof General image files are installed. Ends with slash.
Where Proof General Info files are installed. Ends with slash.
After defining these settings, we define a mode stub for each
proof assistant enabled. The mode stub will autoload Proof General for
the right proof assistant when a file is visited with the corresponding
extension. The proof assistants enabled are the ones listed
in the proof-assistants setting.
Choice of proof assistants to use with Proof General.
A list of symbols chosen from: 'isar 'lego 'coq 'phox 'ccc 'acl2 'plastic 'lclam 'pgshell.
If nil, the default will be ALL proof assistants.
Each proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. To avoid accidently invoking a proof assistant you don't have, only select the proof assistants you (or your site) may need.
You can select which proof assistants you want by setting this variable before `proof-site.el' is loaded, or by setting the environment variable `PROOFGENERAL_ASSISTANTS' to the symbols you want, for example "lego isa". Or you can edit the file `proof-site.el' itself.
Note: to change proof assistant, you must start a new Emacs session.
The default value is nil.
The file `proof-site.el' also defines a version variable.
Version string identifying Proof General release.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The file `proof-config.el' defines the configuration variables for Proof General, including instantiation parameters and user options. See previous chapters for details of its contents. Here we mention some conventions for declaring user options.
Global user options and instantiation parameters are declared using
defcustom as usual. User options should have `*' as the
first character of their docstrings (standard Emacs convention) and live
in the customize group proof-user-options. See
`proof-config.el' for the groups for instantiation parameters.
User options which are generic (having separate instances for each
prover) and instantiation parameters (by definition generic) can be
declared using the special macro defpgcustom. It is used in the
same way as defcustom, except that the symbol declared will
automatically be prefixed by the current proof assistant symbol.
Define a new customization variable <PA>-sym for the current proof assistant.
The function proof-assistant-<SYM> is also defined, which can be used in the
generic portion of Proof General to set and retrieve the value for the current p.a.
Arguments as for `defcustom', which see.
Usage: (defpgcustom SYM &rest args).
In specific instances of Proof General, the macro defpgdefault
can be used to give a default value for a generic setting.
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)
All new instantiation variables are best declared using the
defpgcustom mechanism (old code may be converted gradually).
Customizations which are liable to be different for different instances
of Proof General are also best declared in this way. An example is the
use of X Symbol, controlled by PA-x-symbol-enable, since
it works poorly or not at all with some provers.
To access the generic settings, the following four functions and macros are useful.
Return the value for SYM for the current prover.
Return the symbol for SYM for the current prover. SYM not evaluated.
Return the symbol for SYM for the current prover. SYM is evaluated.
If changing a user option setting amounts to more than just setting a
variable (it may have some dynamic effect), we can set the
custom-set property for the variable to the function
proof-set-value which does an ordinary set-default to set
the variable, and then calls a function with the same name as the
variable, to do whatever is necessary according to the new value for the
variable.
There are several settings which can be switched on or off by the user,
which use this proof-set-value mechanism. They are controlled by
boolean variables with names like proof-foo-enable, and
appear at the start of the customize group proof-user-options.
They should be edited by the user through the customization mechanism,
and set in the code using customize-set-variable.
In proof-utils.el there is a handy macro,
proof-deftoggle, which constructs an interactive function
for toggling boolean customize settings. We can use this to make an
interactive function proof-foo-toggle to put on a menu or
bind to a key, for example.
This general scheme is followed as far as possible, to give uniform
behaviour and appearance for boolean user options, as well as
interfacing properly with the customize mechanism.
Set a customize variable using set-default and a function.
We first call `set-default' to set SYM to value.
Then if there is a function SYM (i.e. with the same name as the
variable SYM), it is called to take some dynamic action for the new
setting.
If there is no function SYM, we try stripping
proof-assistant-symbol and adding "proof-" instead to get
a function name. This extends proof-set-value to work with
generic individual settings.
The dynamic action call only happens when values change: as an approximation we test whether proof-config is fully-loaded yet.
Define a function VAR-toggle for toggling a boolean customize setting VAR.
The toggle function uses customize-set-variable to change the variable.
othername gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Global variables are defined in `proof.el'. The same file defines a few utility functions and some triggers to load in the other files.
The currently active scripting buffer or nil if none.
Process buffer where the proof assistant is run.
The response buffer.
The goals buffer.
Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.
List of files currently included in proof process.
This list contains files in canonical truename format
(see `file-truename').
Whenever a new file is being processed, it gets added to this list
via the proof-shell-process-file configuration settings.
When the prover retracts a file, this list is resynchronised via the
proof-shell-retract-files-regexp and proof-shell-compute-new-files-list
configuration settings.
Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.
NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.
Flag indicating that a completed proof has just been observed.
If non-nil, the value counts the commands from the last command
of the proof (starting from 1).
Flag indicating that an error or interrupt has just occurred.
Set to 'error or 'interrupt if one was observed from the proof
assistant during the last group of commands.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The file `proof-script.el' contains the main code for proof script mode, as well as definitions of menus, key-bindings, and user-level functions.
Proof scripts have two important variables for the locked and queue regions. These variables are local to each script buffer (although we only really need one queue span in total rather than one per buffer).
The locked span of the buffer.
Each script buffer has its own locked span, which may be detached
from the buffer.
Proof General allows buffers in other modes also to be locked;
these also have a non-nil value for this variable.
The queue span of the buffer. May be detached if inactive or empty.
Each script buffer has its own queue span, although only the active
scripting buffer may have an active queue span.
Various utility functions manipulate and examine the spans. An
important one is proof-init-segmentation.
Initialise the queue and locked spans in a proof script buffer.
Allocate spans if need be. The spans are detached from the
buffer, so the regions are made empty by this function.
Also clear list of script portions.
For locking files loaded by a proof assistant, we use the next function.
Make sure buffer is marked as completely processed, completing with a single step.
If buffer already contains a locked region, only the remainder of the buffer is closed off atomically.
This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only.
Atomic locking is instigated by the next function, which uses the
variables proof-included-files-list documented earlier
(see section Handling Multiple Files and see section Global variables).
Register a possibly new file as having been processed by the prover.
If informprover is non-nil, the proof assistant will be told about this, to co-ordinate with its internal file-management. (Otherwise we assume that it is a message from the proof assistant which triggers this call). In this case, the user will be queried to save some buffers, unless noquestions is non-nil.
No action is taken if the file is already registered.
A warning message is issued if the register request came from the proof assistant and Emacs has a modified buffer visiting the file.
An important pair of functions activate and deactivate scripting for the
current buffer. A change in the state of active scripting can trigger
various actions, such as starting up the proof assistant, or altering
proof-included-files-list.
Ready prover and activate scripting for the current script buffer.
The current buffer is prepared for scripting. No changes are
necessary if it is already in Scripting minor mode. Otherwise, it
will become the new active scripting buffer, provided scripting can be
switched off in the previous active scripting buffer with
`proof-deactivate-scripting'.
Activating a new script buffer may be a good time to ask if the user
wants to save some buffers; this is done if the user option
`proof-query-file-save-when-activating-scripting' is set and provided
the optional argument nosaves is non-nil.
The optional argument queuemode relaxes the test for a busy proof shell to allow one which has mode queuemode. In all other cases, a proof shell busy error is given.
Finally, the hooks `proof-activate-scripting-hook' are run. This can
be a useful place to configure the proof assistant for scripting in a
particular file, for example, loading the correct theory, or whatever.
If the hooks issue commands to the proof assistant (via
`proof-shell-invisible-command') which result in an error, the
activation is considered to have failed and an error is given.
Deactivate scripting for the active scripting buffer.
Set `proof-script-buffer' to nil and turn off the modeline indicator.
No action if there is no active scripting buffer.
We make sure that the active scripting buffer either has no locked
region or a full locked region (everything in it has been processed).
If this is not already the case, we question the user whether to
retract or assert, or automatically take the action indicated in the
user option `proof-auto-action-when-deactivating-scripting.'
If the scripting buffer is (or has become) fully processed, and it is
associated with a file, it is registered on
`proof-included-files-list'. Conversely, if it is (or has become)
empty, we make sure that it is not registered. This is to be
certain that the included files list behaves as we might expect with
respect to the active scripting buffer, in an attempt to harmonize
mixed scripting and file reading in the prover.
This function either succeeds, fails because the user refused to
process or retract a partly finished buffer, or gives an error message
because retraction or processing failed. If this function succeeds,
then `proof-script-buffer' is nil afterwards.
The optional argument forcedaction overrides the user option
`proof-auto-action-when-deactivating-scripting' and prevents
questioning the user. It is used to make a value for
the `kill-buffer-hook' for scripting buffers, so that when
a scripting buffer is killed it is always retracted.
The function proof-segment-up-to is the main one used for parsing
the proof script buffer. There are several variants of this function
available corresponding to different parsing strategies; the appropriate
one is aliased to proof-segment-up-to according to which
configuration variables have been set. If only
proof-script-command-end-regexp or proof-terminal-char are set,
then the default is proof-segment-up-to-cmdend. If
proof-script-command-start-regexp is set, the choice is
proof-segment-up-to-cmdstart.
Parse the script buffer from end of locked to pos.
Return a list of (type, string, int) tuples.
Each tuple denotes the command and the position of its terminator,
type is one of 'comment, or 'cmd. 'unclosed-comment may be consed onto
the start if the segment finishes with an unclosed comment.
If optional next-command-end is non-nil, we include the command which continues past pos, if any.
This version is used when `proof-script-command-end-regexp' is set.
Parse the script buffer from end of locked to pos.
Return a list of (type, string, int) tuples.
Each tuple denotes the command and the position of its terminator,
type is one of 'comment, or 'cmd.
If optional next-command-end is non-nil, we include the command which continues past pos, if any. (NOT implemented IN this version).
This version is used when `proof-script-command-start-regexp' is set.
The function proof-semis-to-vanillas is used to convert
a parsed region of the script into a series of commands to
be sent to the proof assistant.
Convert a sequence of terminator positions to a set of vanilla extents.
Proof terminator positions semis has the form returned by
the function proof-segment-up-to.
Set the callback to callback-fn or 'proof-done-advancing by default.
The function proof-assert-until-point is the main one used to
process commands in the script buffer. It's actually used to implement
the assert-until-point, electric terminator keypress, and
find-next-terminator behaviours. In different cases we want different
things, but usually the information (i.e. are we inside a comment) isn't
available until we've actually run proof-segment-up-to (point),
hence all the different options when we've done so.
Process the region from the end of the locked-region until point.
Default action if inside a comment is just process as far as the start of
the comment.
If you want something different, put it inside unclosed-comment-fun. If ignore-proof-process-p is set, no commands will be added to the queue and the buffer will not be activated for scripting.
proof-assert-next-command is a variant of this function.
Process until the end of the next unprocessed command after point.
If inside a comment, just process until the start of the comment.
If you want something different, put it inside unclosed-comment-fun. If ignore-proof-process-p is set, no commands will be added to the queue. Afterwards, move forward to near the next command afterwards, unless dont-move-forward is non-nil. If for-new-command is non-nil, a space or newline will be inserted automatically.
The main command for retracting parts of a script is
proof-retract-until-point.
Set up the proof process for retracting until point.
In particular, set a flag for the filter process to call
`proof-done-retracting' after the proof process has successfully
reset its state.
If delete-region is non-nil, delete the region in the proof script
corresponding to the proof command sequence.
If invoked outside a locked region, undo the last successfully processed
command.
To clean up when scripting is stopped, a script buffer is killed, or the
proof assistant exits, we use the functions
proof-restart-buffers and
proof-script-remove-all-spans-and-deactivate.
Remove all extents in buffers and maybe reset `proof-script-buffer'.
No effect on a buffer which is nil or killed. If one of the buffers
is the current scripting buffer, then `proof-script-buffer'
will deactivated.
Remove all spans from scripting buffers via proof-restart-buffers.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The proof shell mode code is in the file `proof-shell.el'. Proof
shell mode is defined to inherit from comint-mode using
define-derived-mode near the end of the file. The bulk of the
code in the file is concerned with sending code to and from the shell,
and processing output for the associated buffers (goals and response).
Good process handling is a tricky issue. Proof General attempts to manage the process strictly, by maintaining a queue of commands to send to the process. Once a command has been processed, another one is popped off the queue and sent.
There are several important internal variables which control interaction with the process.
A lock indicating that the proof shell is processing.
When this is non-nil, proof-shell-ready-prover will give
an error.
Marker in proof shell buffer pointing to previous command input.
A list of
(span command action)
triples, which is a queue of things to do.
See the functions `proof-start-queue' and `proof-exec-loop'.
Choice of syntax tree encoding for terms.
If nil, prover is expected to make no optimisations. If non-nil, the pretty printer of the prover only reports local changes. For lego 1.3.1 use `nil', for Coq 6.2, use `t'.
The function proof-shell-start is used to initialise a shell
buffer and the associated buffers.
Initialise a shell-like buffer for a proof assistant.
Also generates goal and response buffers. Does nothing if proof assistant is already running.
The function proof-shell-kill-function performs the converse
function of shutting things down; it is used as a hook function for
kill-buffer-hook. Then no harm occurs if the user kills the
shell directly, or if it is done more cautiously via
proof-shell-exit. The function proof-shell-restart allows
a less drastic way of restarting scripting, other than killing and
restarting the process.
Function run when a proof-shell buffer is killed.
Attempt to shut down the proof process nicely and
clear up all the locked regions and state variables.
Value for `kill-buffer-hook' in shell buffer.
Also called by `proof-shell-bail-out' if the process is
exited by hand (or exits by itself).
Query the user and exit the proof process.
This simply kills the `proof-shell-buffer' relying on the hook function
`proof-shell-kill-function' to do the hard work.
Value for the process sentinel for the proof assistant process.
If the proof assistant dies, run proof-shell-kill-function to
cleanup and remove the associated buffers. The shell buffer is
left around so the user may discover what killed the process.
Clear script buffers and send `proof-shell-restart-cmd'.
All locked regions are cleared and the active scripting buffer
deactivated.
If the proof shell is busy, an interrupt is sent with
`proof-interrupt-process' and we wait until the process is ready.
The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.
It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Lego and Coq).
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Input to the proof shell via the queue region is managed by the
functions proof-start-queue and proof-shell-exec-loop.
Begin processing a queue of commands in alist.
If start is non-nil, start and end are buffer positions in the
active scripting buffer for the queue region.
This function calls `proof-append-alist'.
Chop off the vacuous prefix of the command queue alist and queue it.
For each `proof-no-command' item at the head of the list, invoke its
callback and remove it from the list.
Append the result onto `proof-action-list', and if the proof
shell isn't already busy, grab the lock with queuemode and
start processing the queue.
If the proof shell is busy when this function is called, then queuemode must match the mode of the queue currently being processed.
Process the `proof-action-list'.
`proof-action-list' contains a list of (span command action) triples.
If this function is called with a non-empty proof-action-list, the
head of the list is the previously executed command which succeeded.
We execute (action span) on the first item, then (action span) on any
following items which have `proof-no-command' as their cmd components.
If a there is a next command after that, send it to the process. If
the action list becomes empty, unlock the process and remove the queue
region.
The return value is non-nil if the action list is now empty.
Input is actually inserted into the shell buffer and sent to the process
by the low-level function proof-shell-insert.
Insert string at the end of the proof shell, call `comint-send-input'.
First call `proof-shell-insert-hook'. The argument action may be
examined by the hook to determine how to process the string variable.
Then strip string of carriage returns before inserting it and updating
`proof-marker' to point to the end of the newly inserted text.
Do not use this function directly, or output will be lost. It is only
used in `proof-append-alist' when we start processing a queue, and in
`proof-shell-exec-loop', to process the next item.
When Proof General is processing a queue of commands, the lock is managed using a couple of utility functions. You should not need to use these directly.
Grab the proof shell lock, starting the proof assistant if need be.
Runs `proof-state-change-hook' to notify state change.
Clears the `proof-shell-error-or-interrupt-seen' flag.
If queuemode is supplied, set the lock to that value.
Release the proof shell lock, with error or interrupt flag err-or-int.
Clear `proof-shell-busy', and set `proof-shell-error-or-interrupt-seen'
to err-or-int.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Two main functions deal with output, proof-shell-process-output
and proof-shell-process-urgent-message. In effect we consider
the output to be two streams intermingled: the "urgent" messages which
have "eager" annotations, as well as the ordinary ruminations from the
prover.
The idea is to conceal as much irrelevant information from the user as
possible; only the remaining output between prompts and after the last
urgent message will be a candidate for the goal or response buffer. The
internal variable proof-shell-urgent-message-marker tracks the
last urgent message seen.
When output is grabbed from the prover process, the first action
is to strip spurious carriage return characters from the end of
lines, if proof-shell-strip-crs-from-output requires it.
Then the output is stored into
proof-shell-last-output, and its type is stored in
proof-shell-last-output-kind. Output which is deferred or
possibly discarded until the queue is empty is copied into
proof-shell-delayed-output, with type
proof-shell-delayed-output-kind. A record of the last prompt
seen from the prover process is also kept, in
proof-shell-last-prompt.
If non-nil, remove carriage returns (^M) at the end of lines from output.
This is enabled for cygwin32 systems by default. You should turn it off
if you don't need it (slight speed penalty).
A record of the last prompt seen from the proof system.
This is the string matched by `proof-shell-annotated-prompt-regexp'.
A record of the last string seen from the proof system.
A symbol denoting the type of the last output string from the proof system.
Specifically:
'interrupt An interrupt message
|
The output corresponding to this will be in proof-shell-last-output.
See also `proof-shell-proof-completed' for further information about
the proof process output, when ends of proofs are spotted.
This variable can be used for instance specific functions which want
to examine proof-shell-last-output.
A copy of proof-shell-last-output held back for processing at end of queue.
A copy of proof-shell-last-output-lind held back for processing at end of queue.
Process shell output (resulting from cmd) by matching on string.
cmd is the first part of the `proof-action-list' that lead to this
output. The result of this function is a pair (symbol newstring).
Here is where we recognizes interrupts, abortions of proofs, errors, completions of proofs, and proof step hints (proof by pointing results). They are checked for in this order, using
` |
All other output from the proof engine will be reported to the user in
the response buffer by setting `proof-shell-delayed-output' to a cons
cell of ('insert . text) where text is the text string to be inserted.
Order of testing is: interrupt, abort, error, completion.
To extend this function, set `proof-shell-process-output-system-specific'.
The "aborted" case is intended for killing off an open proof during
retraction. Typically it matches the message caused by a
`proof-kill-goal-command'. It simply inserts the word "Aborted" into
the response buffer. So it is expected to be the result of a
retraction, rather than the indication that one should be made.
This function sets `proof-shell-last-output' and `proof-shell-last-output-kind',
which see.
Marker in proof shell buffer pointing to end of last urgent message.
Analyse urgent message for various cases.
Cases are: included file, retracted file, cleared response buffer,
variable setting or dependency list.
If none of these apply, display message.
message should be a string annotated with
`proof-shell-eager-annotation-start', `proof-shell-eager-annotation-end'.
The main processing point which triggers other actions is
proof-shell-filter.
Filter for the proof assistant shell-process.
A function for `comint-output-filter-functions'.
Deal with output and issue new input from the queue.
Handle urgent messages first. As many as possible are processed,
using the function `proof-shell-process-urgent-messages'.
Otherwise wait until an annotated prompt appears in the input.
If `proof-shell-wakeup-char' is set, wait until we see that in the
output chunk str. This optimizes the filter a little bit.
If a prompt is seen, run `proof-shell-process-output' on the output
between the new prompt and the last input (position of `proof-marker')
or the last urgent message (position of
`proof-shell-urgent-message-marker'), whichever is later.
For example, in this case:
PROMPT> input
output-1 urgent-message output-2 PROMPT> |
`proof-marker' is set after input by `proof-shell-insert' and
`proof-shell-urgent-message-marker' is set after urgent-message.
Only output-2 will be processed. For this reason, error
messages and interrupt messages should not be considered
urgent messages.
Output is processed using the function
`proof-shell-filter-process-output'.
The first time that a prompt is seen, `proof-marker' is
initialised to the end of the prompt. This should
correspond with initializing the process. The
ordinary output before the first prompt is ignored (urgent messages,
however, are always processed; hence their name).
Subroutine of `proof-shell-filter' to process output string.
Appropriate action is taken depending on what
`proof-shell-process-output' returns: maybe handle an interrupt, an
error, or deal with ordinary output which is a candidate for the goal
or response buffer. Ordinary output is only displayed when the proof
action list becomes empty, to avoid a confusing rapidly changing
output.
After processing the current output, the last step undertaken by the filter is to send the next command from the queue.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
To debug Proof General, it may be helpful to set the
configuration variable proof-show-debug-messages.
Whether to display debugging messages in the response buffer.
If non-nil, debugging messages are displayed in the response giving
information about what Proof General is doing.
To avoid erasing the messages shortly after they're printed,
you should set `proof-tidy-response' to nil.
The default value is nil.
For more information about debugging Emacs lisp, consult the Emacs Lisp
Reference Manual. I recommend using the source-level debugger
edebug.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.