10. Configuring Font Lock
Support for Font Lock in Proof General is described in the user manual
(see the Syntax highlighting section). To configure Font Lock for a
new proof assistant, you need to set the variable
font-lock-keywords in each of the mode functions you want
highlighting for. Proof General will automatically install these
settings, and use font lock minor mode (for syntax highlighting as you
type) in script buffers.
To understand its format, check the documentation of
font-lock-keywords inside Emacs.
Instead of setting font-lock-keywords in each mode function, you
can use the following four variables to make the settings in place.
This is particularly useful if use the easy configuration mechanism for
Proof General, see section Demonstration instance and easy configuration.
- Variable: proof-script-font-lock-keywords
Value of ‘
font-lock-keywords’ used to fontify proof scripts.
The proof script mode should set this before calling ‘proof-config-done’. Used also by ‘proof-easy-config’ mechanism. See also ‘proof-goals-font-lock-keywords’ and ‘proof-response-font-lock-keywords’.
- Variable: proof-goals-font-lock-keywords
Value of ‘
font-lock-keywords’ used to fontify the goals output.
The goals shell mode should set this before calling ‘proof-goals-config-done’. Used also by ‘proof-easy-config’ mechanism. See also ‘proof-script-font-lock-keywords’ and ‘proof-response-font-lock-keywords’.
- Variable: proof-response-font-lock-keywords
Value of ‘
font-lock-keywords’ used to fontify the response output.
The response mode should set this before calling ‘proof-response-config-done’. Used also by ‘proof-easy-config’ mechanism. See also ‘proof-script-font-lock-keywords’ and ‘proof-goals-font-lock-keywords’.
Proof General provides a special function, proof-zap-commas, for
tweaking the font lock behaviour of provers which have declarations of
the form x,y,z:Ty. This function removes highlighting on the
commas, and can be added as the last element of
font-lock-keywords. Further manipulation of font lock behaviour
can be achieved via two hook functions which are run before and after
fontifying the output buffers.
- Function: proof-zap-commas limit
Remove the face of all ‘,’ from point to limit.
Meant to be used from ‘font-lock-keywords’ as a way to unfontify commas in declarations and definitions. Useful for provers which have declarations of the form x,y,z:Ty All that can be said for it is that the previous ways of doing this were even more bogus....
- Variable: pg-before-fontify-output-hook
This hook is called before fontifying a region in an output buffer.
A function on this hook can alter the region of the buffer within the current restriction, and must return the final value of (point-max). [This hook is presently only used by phox-sym-lock].
- Variable: pg-after-fontify-output-hook
This hook is called before fonfitying a region in an output buffer.
[This hook is presently only used by Isabelle].
This document was generated on November 21, 2024 using texi2html 1.82.