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.

Variable: pg-subterm-sep-char: Finishing special for a subterm markup.
See doc of pg-subterm-start-char.

Variable: pg-topterm-regexp

Annotation regexp 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 could also be a literal command to insert and send back to the prover.

The function pg-topterm-goalhyplit-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 on January 24, 2026 using texi2html 1.82.