5. Goals Buffer Settings

The goals buffer settings allow configuration of Proof General for proof by pointing or similar features. See the Proof General documentation web page for a link to the technical report ECS-LFCS-97-368 which hints at how to use these settings.

Variable: pg-goals-change-goal

Command to change to the goal `%s'

Variable: pbp-goal-command

Command sent when `pg-goals-button-action' is requested on a goal.

Variable: pbp-hyp-command

Command sent when `pg-goals-button-action' is requested on an assumption.

Variable: pg-goals-error-regexp

Regexp indicating that the proof process has identified an error.

Variable: proof-shell-result-start

Regexp matching start of an output from the prover after pbp commands.
In particular, after a `pbp-goal-command' or a `pbp-hyp-command'.

Variable: proof-shell-result-end

Regexp matching end of output from the prover after pbp commands.
In particular, after a `pbp-goal-command' or a `pbp-hyp-command'.

Variable: pg-subterm-start-char

Opening special character for subterm markup.
Subsequent special characters with values below pg-subterm-first-special-char are assumed to be subterm position indicators. Annotations should be finished with pg-subterm-sep-char; the end of the concrete syntax is indicated by pg-subterm-end-char.

If `pg-subterm-start-char' is nil, subterm markup is disabled.

See doc of `pg-goals-analyse-structure' for more details of subterm and proof-by-pointing markup mechanisms..

Variable: pg-subterm-sep-char

Finishing special for a subterm markup.
See doc of `pg-subterm-start-char'.

Variable: pg-topterm-char

Annotation character that indicates the beginning of a "top" element.
A "top" element may be a sub-goal to be proved or a named hypothesis, for example. It is currently assumed (following lego/Coq conventions) to span a whole line.

The function `pg-topterm-goalhyp-fn' examines text following this special character, to determine what kind of top element it is.

This setting is also used to see if proof-by-pointing features are configured. If it is unset, some of the code for parsing the prover output is disabled.

Variable: pg-subterm-end-char

Closing special character for subterm markup.
See `pg-subterm-start-char'.

This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.