Download User manual - Proof General

46
Proof General
proof-general-debug
[User Option]
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.
proof-follow-mode
[User Option]
Choice of how point moves with script processing commands.
One of the symbols: ’locked, ’follow, ’followdown, ’ignore.
If ’locked, point sticks to the end of the locked region. If ’follow, point moves just when
needed to display the locked region end. If ’followdown, point if necessary to stay in writeable region If ’ignore, point is never moved after movement commands or on errors.
If you choose ’ignore, you can find the end of the locked using M-x proof-goto-end-oflocked
The default value is locked.
proof-auto-action-when-deactivating-scripting
[User Option]
If ’retract or ’process, do that when deactivating scripting.
With this option set to ’retract or ’process, when scripting is turned off in a partly
processed buffer, the buffer will be retracted or processed automatically.
With this option unset (nil), the user is questioned instead.
Proof General insists that only one script buffer can be partly processed: all others have to
be completely processed or completely unprocessed. This is to make sure that handling of
multiple files makes sense within the proof assistant.
NB: A buffer is completely processed when all non-whitespace is locked (coloured blue); a
buffer is completely unprocessed when there is no locked region.
For some proof assistants (such as Coq) fully processed buffers make no sense. Setting this
option to ’process has then the same effect as leaving it unset (nil). (This behaviour is
controlled by ‘proof-no-fully-processed-buffer’.)
The default value is nil.
proof-rsh-command
[User Option]
Shell command prefix to run a command on a remote host.
For example,
ssh bigjobs
Would cause Proof General to issue the command ‘ssh bigjobs isabelle’ to start Isabelle
remotely on our large compute server called ‘bigjobs’.
The protocol used should be configured so that no user interaction (passwords, or whatever)
is required to get going. For proper behaviour with interrupts, the program should also
communicate signals to the remote host.
The default value is nil.
8.5 Changing faces
The numerous fonts and colours that Proof General uses are configurable. If you alter faces
through the customize menus (or the command M-x customize-face), only the particular kind
of display in use (colour window system, monochrome window system, console, . . . ) will be affected. This means you can keep separate default settings for each different display environment
where you use Proof General.