[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# 13. Internals of Proof General

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.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 13.1 Spans

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] | [ ? ]

## 13.2 Proof General site configuration

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.

Variable: proof-home-directory

  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.

Variable: proof-images-directory

  Where Proof General image files are installed. Ends with slash.

Variable: proof-info-directory

  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.

User Option: proof-assistants

  Choice of proof assistants to use with Proof General.
  A list of symbols chosen from: `'isar` `'coq` `'phox` `'lego` `'plastic`. If nil, the default will be ALL available 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.

Variable: proof-general-version

  Version string identifying Proof General release.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 13.3 Configuration variable mechanisms

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.

Macro: defpgcustom

  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.

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)

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.

Macro: proof-ass

  Return the value for SYM for the current prover.
  This macro should only be invoked once a specific prover is engaged.

Macro: proof-ass-sym

  Return the symbol for SYM for the current prover. SYM not evaluated.
  This macro should only be called once a specific prover is known.

Macro: proof-ass-symv

  Return the symbol for SYM for the current prover. SYM evaluated.
  This macro should only be invoked once a specific prover is engaged.

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.

Function: proof-set-value sym value

  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.

Macro: proof-deftoggle

  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] | [ ? ]

## 13.4 Global variables

Global variables are defined in ‘`proof.el`’. The same file defines a few utility functions and some triggers to load in the other files.

Variable: proof-script-buffer

  The currently active scripting buffer or nil if none.

Variable: proof-shell-buffer

  Process buffer where the proof assistant is run.

Variable: proof-response-buffer

  The response buffer.

Variable: proof-goals-buffer

  The goals buffer.

Variable: proof-buffer-type

  Symbol for the type of this buffer: `'script`, `'shell`, `'goals`, or `'response`.

Variable: proof-included-files-list

  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.

Variable: proof-shell-proof-completed

  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).

Variable: proof-shell-error-or-interrupt-seen

  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] | [ ? ]

## 13.5 Proof script mode

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).

Variable: proof-locked-span

  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.

Variable: proof-queue-span

  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`.

Function: 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.

Function: proof-complete-buffer-atomic buffer

  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).

Function: proof-register-possibly-new-processed-file file &optional informprover noquestions

  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`.

Command: proof-activate-scripting &optional nosaves queuemode

  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.

Command: proof-deactivate-scripting &optional forcedaction

  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`.

Function: proof-segment-up-to-cmdend pos &optional next-command-end

  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.

Function: proof-segment-up-to-cmdstart pos &optional next-command-end

  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.

Function: proof-semis-to-vanillas semis &optional callback-fn

  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.

Function: proof-assert-until-point &optional unclosed-comment-fun ignore-proof-process-p

  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.

Command: proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command

  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`.

Function: proof-retract-until-point &optional delete-region

  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`.

Function: proof-restart-buffers buffers

  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.

Function: proof-script-remove-all-spans-and-deactivate

  Remove all spans from scripting buffers via `proof-restart-buffers`.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 13.6 Proof shell mode

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.

Variable: proof-shell-busy

  A lock indicating that the proof shell is processing.
  When this is non-nil, `proof-shell-ready-prover` will give an error.

Variable: proof-marker

  Marker in proof shell buffer pointing to previous command input.

Variable: proof-action-list

  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`’.

Variable: pg-subterm-anns-use-stack

  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.

Command: proof-shell-start

  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: proof-shell-kill-function

  Function run when a proof-shell buffer is killed.
  Try to shut down the proof process nicely and clear locked regions and state variables. Value for ‘``kill-buffer-hook``’ in shell buffer, alled by ‘``proof-shell-bail-out``’ if process exits.

Command: proof-shell-exit

  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.

Function: proof-shell-bail-out process event

  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.

Command: proof-shell-restart

  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] | [ ? ]

### 13.6.1 Input to the shell

Input to the proof shell via the queue region is managed by the functions `proof-start-queue` and `proof-shell-exec-loop`.

Function: proof-start-queue start end alist

  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``’.

Function: proof-append-alist alist &optional queuemode

  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.

Function: proof-shell-exec-loop

  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`.

Function: proof-shell-insert string action

  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. NB: the hook is not called for the empty (null) string.

  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.

Function: proof-grab-lock &optional queuemode

  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.

Function: proof-release-lock &optional err-or-int

  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] | [ ? ]

### 13.6.2 Output from the shell

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`.

Variable: proof-shell-strip-crs-from-output

  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).

Variable: proof-shell-last-prompt

  A raw record of the last prompt seen from the proof system.
  This is the string matched by ‘``proof-shell-annotated-prompt-regexp``’.

Variable: proof-shell-last-output

  A record of the last string seen from the proof system.
  This is raw string, for internal use only.

Variable: proof-shell-last-output-kind

  A symbol denoting the type of the last output string from the proof system.
  Specifically:

       'interrupt      An interrupt message
       'error          An error message
       'abort          A proof abort message
       'loopback       A command sent from the PA to be inserted into the script
       'response       A response message
       'goals          A goals (proof state) display
       'systemspecific Something specific to a particular system,
                        -- see ‘proof-shell-process-output-system-specific’

  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`.

Variable: proof-shell-delayed-output

  A copy of `proof-shell-last-output` held back for processing at end of queue.

Variable: proof-shell-delayed-output-kind

  A copy of proof-shell-last-output-lind held back for processing at end of queue.

Function: proof-shell-process-output cmd string

  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

        ‘proof-shell-interrupt-regexp’
        ‘proof-shell-error-regexp’
        ‘proof-shell-abort-goal-regexp’
        ‘proof-shell-proof-completed-regexp’
        ‘proof-shell-result-start’

  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.

Variable: proof-shell-urgent-message-marker

  Marker in proof shell buffer pointing to end of last urgent message.

Function: proof-shell-process-urgent-message 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`.

Function: proof-shell-filter str

  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).

Function: proof-shell-filter-process-output string

  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] | [ ? ]

## 13.7 Debugging

To debug Proof General, it may be helpful to set the configuration variable `proof-general-debug`.

User Option: proof-general-debug

  Non-nil to run Proof General in debug mode.
  This changes some behaviour (e.g. markup stripping) and displays debugging messages in the response buffer. To avoid erasing messages shortly after they're printed, set ‘``proof-tidy-response``’ to nil. This is only useful for PG developers.

  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 July, 24 2008 using texi2html 1.78.