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

# 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.
  This is currently used only by ‘``proof-easy-config``’ mechanism, to set ‘``font-lock-keywords``’ before calling `proof-config-done`. See also proof-{shell,resp,goals}-`font-lock-keywords`.

Variable: proof-shell-font-lock-keywords

  Value of ‘``font-lock-keywords``’ used to fontify the proof shell.
  This is currently used only by ‘``proof-easy-config``’ mechanism, to set ‘``font-lock-keywords``’ before calling ‘``proof-config-done``’. See also proof-{script,resp,goals}-`font-lock-keywords`.

Variable: proof-goals-font-lock-keywords

  Value of ‘``font-lock-keywords``’ used to fontify the goals output.
  NB: the goals output is not kept in font lock mode because the fontification may rely on annotations which are erased before displaying. This means internal functions of PG must be used to display to the goals buffer to ensure fontification is done! This is currently used only by ‘``proof-easy-config``’ mechanism, to set ‘``font-lock-keywords``’ before calling `proof-config-done`. See also proof-{script,shell,resp}-`font-lock-keywords`.

Variable: proof-resp-font-lock-keywords

  Value of ‘``font-lock-keywords``’ used to fontify the response output.
  NB: the goals output is not kept in font lock mode because the fontification may rely on annotations which are erased before displaying. This means internal functions of PG must be used to display to the goals buffer to ensure fontification is done! This is currently used only by `proof-easy-config` mechanism, to set `font-lock-keywords` before calling `proof-config-done`. See also proof-{script,shell,resp}-`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``’.

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

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

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.