Download Adapting manual

Chapter 14: Internals of Proof General
proof-ass-sym
53
[Macro]
Return the symbol for SYM for the current prover. SYM not evaluated.
This macro should only be called once a specific prover is known.
proof-ass-symv
[Macro]
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 proofset-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-setvalue 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-setvariable.
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.
proof-set-value sym value
[Function]
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]
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.
proof-deftoggle
14.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.
proof-script-buffer
[Variable]
The currently active scripting buffer or nil if none.
proof-shell-buffer
[Variable]
Process buffer where the proof assistant is run.
proof-response-buffer
The response buffer.
[Variable]