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 November 21, 2024 using texi2html 1.82.